From 479d45e679e8486c65b77f2ddfa8718c24778a75 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 8 Oct 2015 11:00:22 +0200 Subject: f_equal fix continued: do a refresh_universes as before. --- plugins/cc/cctac.ml | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index cbd95eaea..068cb25cf 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -483,24 +483,26 @@ let congruence_tac depth l = 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) +let mk_eq f c1 c2 k = + Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> + Proofview.Goal.enter begin + fun gl -> + let open Tacmach.New in + let evm, ty = pf_apply type_of gl c1 in + let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in + let term = mkApp (fc, [| ty; c1; c2 |]) in + let evm, _ = type_of (pf_env gl) evm term in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) + (k term) end) - + let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_unsafe_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) - let ty = (* Termops.refresh_universes *) (type_of c1) in Tacticals.New.tclTHEN - ((new_app_global_check _eq [|ty; c1; c2|]) Tactics.cut) + (mk_eq _eq 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 -- cgit v1.2.3