Quelle  ltac2_var_quot.out   Sprache: unbekannt

Rocq < Rocq < Toplevel input, characters 7-9:
> Check $x.
>       ^^
Error: Unbound value x

Rocq < Rocq < Toplevel input, characters 16-17:
> Check $preterm:x.
>                ^
Error: Unbound value x

Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ x.
>       ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).

Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm:x.
>       ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).

Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm : x.
>       ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).

Rocq < Rocq < Toplevel input, characters 18-19:
> Check $preterm : x.
>                  ^
Error: The reference x was not found in the current environment.

Rocq < Rocq < Toplevel input, characters 16-24:
> Check fun x => $preterm : x.
>                ^^^^^^^^
Error: Unbound value preterm

Rocq < Rocq < Toplevel input, characters 17-18:
> Check $preterm: x.
>                 ^
Error: The reference x was not found in the current environment.

Rocq < Rocq < Toplevel input, characters 16-24:
> Check fun x => $preterm: x.
>                ^^^^^^^^
Error: Unbound value preterm

Rocq < Rocq < Toplevel input, characters 7-8:
> Check $ preterm :x.
>       ^
Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).

Rocq <