Fix bug #3593, making constr_eq and progress work up to

equality of universes, along with a few other functions in evd.

5 files changed, 28 insertions, 21 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0f1d7cb027..6fa4342d34 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -146,14 +146,14 @@ let eq_pri_auto_tactic (_, x) (_, y) =
   if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
     match x.code,y.code with
       | Res_pf (cstr,_),Res_pf (cstr1,_) -> 
-	   eq_constr cstr cstr1
+	  Term.eq_constr cstr cstr1
       | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> 
-	  eq_constr cstr cstr1
+	  Term.eq_constr cstr cstr1
       | Give_exact (cstr,_),Give_exact (cstr1,_)  -> 
-	  eq_constr cstr cstr1
+	  Term.eq_constr cstr cstr1
       | Res_pf_THEN_trivial_fail (cstr,_)
 	  ,Res_pf_THEN_trivial_fail (cstr1,_) -> 
-	  eq_constr cstr cstr1
+	  Term.eq_constr cstr cstr1
       | _,_ -> false
   else
     false
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7de9330ba6..881bb5c621 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -249,7 +249,7 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
       | _ ->
 	  let env' = Environ.push_rel_context ctx env in
 	  let ty' = whd_betadeltaiota env' ar in
-	       if not (eq_constr ty' ar) then iscl env' ty'
+	       if not (Term.eq_constr ty' ar) then iscl env' ty'
 	       else false
   in
   let is_class = iscl env cty in
@@ -278,13 +278,14 @@ let pf_filtered_hyps gls =
   Goal.V82.hyps gls.Evd.sigma (sig_it gls)
 
 let make_hints g st only_classes sign =
+  let sigma = project g in
   let paths, hintlist =
     List.fold_left
     (fun (paths, hints) hyp ->
       let consider =
 	try let (_, b, t) = Global.lookup_named (pi1 hyp) in
 	      (* Section variable, reindex only if the type changed *)
-	      not (eq_constr t (pi3 hyp))
+	      not (eq_constr sigma t (pi3 hyp))
 	with Not_found -> true
      in
       if consider then 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4020a93fd3..c524e67ce7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1588,8 +1588,8 @@ let is_eq_x gl x (id,_,c) =
   try
     let c = pf_nf_evar gl c in
     let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in
-    if (eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
-    if (eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
+    if (Term.eq_constr x lhs) && not (occur_term x rhs) then raise (FoundHyp (id,rhs,true));
+    if (Term.eq_constr x rhs) && not (occur_term x lhs) then raise (FoundHyp (id,lhs,false))
   with ConstrMatching.PatternMatchingFailure ->
     ()
 
@@ -1679,7 +1679,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
       let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
       if flags.only_leibniz then restrict_to_eq_and_identity eq;
       (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
-      if eq_constr x y then failwith "caught";
+      if Term.eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ ->
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
     with ConstrMatching.PatternMatchingFailure -> failwith "caught"
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 41f8dc8dec..c1e6f42f1c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -777,9 +777,14 @@ END
 
 (* ********************************************************************* *)
 
+let eq_constr x y = 
+  Proofview.Goal.enter (fun gl ->
+    let evd = Proofview.Goal.sigma gl in
+      if Evd.eq_constr evd x y then Proofview.tclUNIT () 
+      else Tacticals.New.tclFAIL 0 (str "Not equal"))
+
 TACTIC EXTEND constr_eq
-| [ "constr_eq" constr(x) constr(y) ] -> [
-    if eq_constr x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
+| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ]
 END
 
 TACTIC EXTEND constr_eq_nounivs
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a495c8783e..28e0b72623 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1124,7 +1124,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let hypclause = mk_clenv_from_env env sigma (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
-  if eq_constr hyp_typ new_hyp_typ then
+  if eq_constr sigma hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
@@ -3065,14 +3065,14 @@ let specialize_eqs id gl =
     match kind_of_term ty with
     | Prod (na, t, b) ->
 	(match kind_of_term t with
-	| App (eq, [| eqty; x; y |]) when eq_constr (Lazy.force coq_eq) eq ->
+	| App (eq, [| eqty; x; y |]) when eq_constr !evars (Lazy.force coq_eq) eq ->
 	    let c = if noccur_between 1 (List.length ctx) x then y else x in
 	    let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
 	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
 	      if unif (push_rel_context ctx env) evars pt t then
 		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
 	      else acc, in_eqs, ctx, ty
-	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr !evars heq (Lazy.force coq_heq) ->
 	    let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
 	    let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
 	    let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
@@ -3262,16 +3262,16 @@ let compute_scheme_signature scheme names_info ind_type_guess =
       | Some (_,Some _,_) ->
 	  error "Strange letin, cannot recognize an induction scheme."
       | None -> (* Non standard scheme *)
-	  let cond hd = eq_constr hd ind_type_guess && not scheme.farg_in_concl
+	  let cond hd = Term.eq_constr hd ind_type_guess && not scheme.farg_in_concl
 	  in (cond, fun _ _ -> ())
       | Some ( _,None,ind) -> (* Standard scheme from an inductive type *)
 	  let indhd,indargs = decompose_app ind in
-	  let cond hd = eq_constr hd indhd in
+	  let cond hd = Term.eq_constr hd indhd in
 	  let check_concl is_pred p =
 	    (* Check again conclusion *)
 	    let ccl_arg_ok = is_pred (p + scheme.nargs + 1) f == IndArg in
 	    let ind_is_ok =
-	      List.equal eq_constr
+	      List.equal Term.eq_constr
 		(List.lastn scheme.nargs indargs)
 		(extended_rel_list 0 scheme.args) in
 	    if not (ccl_arg_ok && ind_is_ok) then
@@ -4030,10 +4030,10 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
    is solved by tac *)
 
 (** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl d1 d2 = match d2,d1 with
+let interpretable_as_section_decl evd d1 d2 = match d2,d1 with
   | (_,Some _,_), (_,None,_) -> false
-  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2
-  | (_,None,t1), (_,_,t2) -> eq_constr t1 t2
+  | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr evd b1 b2 && eq_constr evd t1 t2
+  | (_,None,t1), (_,_,t2) -> eq_constr evd t1 t2
 
 let abstract_subproof id gk tac =
   let open Tacticals.New in
@@ -4042,11 +4042,12 @@ let abstract_subproof id gk tac =
   Proofview.Goal.nf_enter begin fun gl ->
   let current_sign = Global.named_context()
   and global_sign = Proofview.Goal.hyps gl in
+  let sigma = Proofview.Goal.sigma gl in
   let sign,secsign =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
 	if mem_named_context id current_sign &&
-          interpretable_as_section_decl (Context.lookup_named id current_sign) d
+          interpretable_as_section_decl sigma (Context.lookup_named id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (add_named_decl d s1,s2))
       global_sign (empty_named_context,empty_named_context_val) in