From e26b4dbedd29acbfb9cbf2320193cc68afa60cf3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 7 Oct 2015 16:51:53 +0200
Subject: Fix bug #4069: f_equal regression.

---
 plugins/cc/cctac.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6439f58d24..cbd95eaeaf 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
-- 
cgit v1.2.3


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(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index cbd95eaeaf..068cb25cf2 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