diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-26 16:37:26 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-27 00:28:50 +0200 |
commit | 05bd0ab1dd85764874ca077005dcaff5414589a5 (patch) | |
tree | 40ecae5fc60a644761898bcb61e13ef463efecb6 /test-suite/bugs/closed/5757.v | |
parent | b818c00e3e895ea9b736ab968e3ba109b0fd67c1 (diff) |
Moving setting of "cleared" evar flag directly in Evd.restrict.
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
Diffstat (limited to 'test-suite/bugs/closed/5757.v')
-rw-r--r-- | test-suite/bugs/closed/5757.v | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5757.v b/test-suite/bugs/closed/5757.v new file mode 100644 index 000000000..0d0f2eed4 --- /dev/null +++ b/test-suite/bugs/closed/5757.v @@ -0,0 +1,76 @@ +(* Check that resolved status of evars follows "restrict" *) + +Axiom H : forall (v : nat), Some 0 = Some v -> True. +Lemma L : True. +eapply H with _; +match goal with + | |- Some 0 = Some ?v => change (Some (0+0) = Some v) +end. +Abort. + +(* The original example *) + +Set Default Proof Using "Type". + +Module heap_lang. + +Inductive expr := + | InjR (e : expr). + +Inductive val := + | InjRV (v : val). + +Bind Scope val_scope with val. + +Fixpoint of_val (v : val) : expr := + match v with + | InjRV v => InjR (of_val v) + end. + +Fixpoint to_val (e : expr) : option val := None. + +End heap_lang. +Export heap_lang. + +Module W. +Inductive expr := + | Val (v : val) + (* Sums *) + | InjR (e : expr). + +Fixpoint to_expr (e : expr) : heap_lang.expr := + match e with + | Val v => of_val v + | InjR e => heap_lang.InjR (to_expr e) + end. + +End W. + + + +Section Tests. + + Context (iProp: Type). + Context (WPre: expr -> Prop). + + Context (tac_wp_alloc : + forall (e : expr) (v : val), + to_val e = Some v -> WPre e). + + Lemma push_atomic_spec (x: val) : + WPre (InjR (of_val x)). + Proof. +(* This works. *) +eapply tac_wp_alloc with _. +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Undo. Undo. +(* This is fixed *) +eapply tac_wp_alloc with _; +match goal with + | |- to_val ?e = Some ?v => + change (to_val (W.to_expr (W.InjR (W.Val x))) = Some v) +end. +Abort. |