Does not allow underscores in assume tactic

[fblanqui]

• tactic: does not allow _ in assume
• sig_state, scope: fix comments

lambdapi-stdlib <= 1.1.0 is not compatible with this change. The master branch of lambdapi-stdlib is compatible with this change (since fe8c1758d469df1c1eabe0a09690603791e819c2 on 31/12/24).

[fblanqui]

@NotBad4U @melanie-taprogge : Is this change a problem for you?

[melanie-taprogge]

@NotBad4U @melanie-taprogge : Is this change a problem for you?

It will not be an issue for me!

[NotBad4U]

Yes, it breaks things on my side. I convert Alethe's ID name, such as t1.t2, into t1_t2.
I plan to use the {|i|} syntax in the future because SMT-LIB is more permissive than Lambdapi for identifiers.
So, that will not impact me in the future, but at this time, yes, it breaks stuff on my side.

But I do not understand why you want to refuse snake case syntax with assume.
What are you trying to do?

[fblanqui]

Hi Alessio. I don't understand your remark. The change is not about forbidding names with underscores but underscore itself which has a special meaning and is not implemented currently anyway.

[fblanqui]

@AntineaOgg : is this change a problem for you?

[NotBad4U]

Hi Alessio. I don't understand your remark. The change is not about forbidding names with underscores but underscore itself which has a special meaning and is not implemented currently anyway.

Oh! Sorry, the comment of the PR misled me. I might have a few _ in some proof when I just want to ignore the name of a variable when I read the proof goal. But I can fix this quickly.

[AntineaOgg]

@AntineaOgg : is this change a problem for you?

Hello, I don't think it will cause troubles for us.