diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 16:51:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2015-10-07 16:51:53 +0200 |
| commit | e26b4dbedd29acbfb9cbf2320193cc68afa60cf3 (patch) | |
| tree | 397f85c4b33d5b7339027371df67f35e09272c6d /plugins/cc | |
| parent | 08a0c44e3525d1f0c7303d189e826e25c3e3d914 (diff) | |
Fix bug #4069: f_equal regression.
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 6439f58d2..cbd95eaea 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -482,6 +482,15 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) + +let new_app_global_check f args k = + new_app_global f args + (fun c -> + Proofview.Goal.enter + begin fun gl -> + let evm, _ = Tacmach.New.pf_apply type_of gl c in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k c) + end) let f_equal = Proofview.Goal.nf_enter begin fun gl -> @@ -490,11 +499,9 @@ let f_equal = let cut_eq c1 c2 = try (* type_of can raise an exception *) let ty = (* Termops.refresh_universes *) (type_of c1) in - if eq_constr_nounivs c1 c2 then Proofview.tclUNIT () - else - Tacticals.New.tclTRY (Tacticals.New.tclTHEN - ((new_app_global _eq [|ty; c1; c2|]) Tactics.cut) - (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply))) + Tacticals.New.tclTHEN + ((new_app_global_check _eq [|ty; c1; c2|]) Tactics.cut) + (Tacticals.New.tclTRY ((new_app_global _refl_equal [||]) apply)) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e in Proofview.tclORELSE |