diff options
author | 2014-11-03 15:23:57 +0100 | |
---|---|---|
committer | 2014-11-03 15:53:49 +0100 | |
commit | c4f270f573360e39bd91e3ffff8d37775b2871d7 (patch) | |
tree | 7419764e14de7287b48f448dde27272beb7eedf5 | |
parent | 7af811e5100839484cbed0126b5c37a972487ec3 (diff) |
Subtle swap of lines to preserve VarInstance src field before checking
for residual unifiable evars (otherwise "thin" from logic.ml, erases
the src field) + typo.
-rw-r--r-- | tactics/tactics.ml | 3 | ||||
-rw-r--r-- | test-suite/success/destruct.v | 7 |
2 files changed, 8 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5918cf997..e26be98b5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3841,11 +3841,10 @@ let pose_induction_arg_then clear_flag isrec with_evars let (sigma,c) = use_bindings env sigma elim (c0,lbind) t0 in let t = Retyping.get_type_of env sigma c in mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)); + Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable); if is_arg_pure_hyp then Tacticals.New.tclTRY (Proofview.V82.tactic (thin [destVar c0])) else Proofview.tclUNIT (); - Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable); - Proofview.shelve_unifiable; if isrec then Proofview.cycle (-1) else Proofview.tclUNIT () ]) (tac fixedvars) diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 0faaa275f..8e9be2e40 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -369,3 +369,10 @@ intros. destruct (H _). change (0=0) in H0. (* Check generalization on H0 was made *) Abort. + +(* Check absence of anomaly (failed at some time) *) + +Goal forall A (a:A) (P Q:A->Prop), (forall a, P a -> Q a) -> True. +intros. +Fail destruct H. +Abort. |