coq

coq copied to clipboard

Description of the problem

Hi, I've just noticed a problem with Reset (which is a great feature for testing while writing code!). Basically, as you see below, I can Reset something that has already been Reset

Fail Reset foo.  (* this fails, as expected*)
Definition blut : nat := 0.
Fail Reset foo. (* idem *)
Reset blut.
Definition blut := 0.
Print blut.
Reset blut.  (* if this line commented, then the Definition below fails *)
Fail Print blut. (* as expected *)

Definition my_id (n : nat) : nat := n.


Print my_id. (* last time it works*)
Reset foo.  (* this should not work *)
Reset blut. (* this should not work *) 
Fail Print my_id.  (* this should work*)

I guess that, since it ignores the resetting of the ident blut, it still resets everything after the first or the second Definition of blut as per the refman i.e. This command removes all the objects in the environment since ident was introduced.

I guess it's a bug since if one wants to check if some anonymous goals type-check without overloading the global environment (or if one simply does not want to find new names each time one make a new test while writing code), it's better to do a series of Lemma foo : ... Qed. Reset foo.s than Goals.

Coq Version

The Coq Proof Assistant, version 8.14.1 compiled with OCaml 4.12.0