introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha AND universe erasure

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11010 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 24 insertions, 12 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5f5b47783a..055d2e51b3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -616,14 +616,6 @@ let pb_equal = function
 
 let sort_cmp = sort_cmp
 
-let base_sort_cmp pb s0 s1 =
-  match (s0,s1) with
-    | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos  (* Prop <= Set *)
-    | (Prop c1, Type u)  -> pb = CUMUL
-    | (Type u1, Type u2) -> true
-    | _ -> false
-
-
 let test_conversion f env sigma x y =
   try let _ = f env (nf_evar sigma x) (nf_evar sigma y) in true
   with NotConvertible -> false
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c9b157efd9..6c029a161f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -201,7 +201,6 @@ val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
 val sort_cmp : conv_pb -> sorts -> sorts -> conversion_test
-val base_sort_cmp : conv_pb -> sorts -> sorts -> bool
 
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index cb6146338c..9a9e25c599 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -939,6 +939,22 @@ let next_name_not_occuring avoid_flags name l env_names t =
         (* invent a valid name *)
         next (id_of_string "H")
 
+let base_sort_cmp pb s0 s1 =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) -> c1 = Null or c2 = Pos  (* Prop <= Set *)
+    | (Prop c1, Type u)  -> pb = Reduction.CUMUL
+    | (Type u1, Type u2) -> true
+    | _ -> false
+
+(* eq_constr extended with universe erasure *)
+let rec constr_cmp cv_pb t1 t2 =
+  (match kind_of_term t1, kind_of_term t2 with
+      Sort s1, Sort s2 -> base_sort_cmp cv_pb s1 s2
+    | _ -> false)
+  || compare_constr (constr_cmp cv_pb) t1 t2
+
+let eq_constr = constr_cmp Reduction.CONV
+
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
 (* Remplace 2 versions précédentes buggées                  *)
@@ -964,6 +980,7 @@ let rec eta_reduce_head c =
            | _ -> c)
     | _ -> c
 
+
 (* alpha-eta conversion : ignore print names and casts *)
 let eta_eq_constr =
   let rec aux t1 t2 =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index aa814442ab..22a370aaf6 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -147,6 +147,10 @@ val subst_term_occ_decl :
 val error_invalid_occurrence : int list -> 'a
 
 (* Alternative term equalities *)
+val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
+val constr_cmp : Reduction.conv_pb -> constr -> constr -> bool
+val eq_constr : constr -> constr -> bool
+
 val eta_reduce_head : constr -> constr
 val eta_eq_constr : constr -> constr -> bool
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a6de33ace4..13587c9d75 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -154,8 +154,8 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
 	(match flags.modulo_conv_on_closed_terms with
 	    Some flags ->
 	      is_trans_fconv (conv_pb_of pb) flags env sigma m n
-	  | None -> eq_constr m n)
-    | _ -> false in
+	  | None -> constr_cmp (conv_pb_of cv_pb) m n)
+    | _ -> constr_cmp (conv_pb_of cv_pb) m n in
   let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn =
     let cM = Evarutil.whd_castappevar sigma curm
     and cN = Evarutil.whd_castappevar sigma curn in 
@@ -247,7 +247,7 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
       (match flags.modulo_conv_on_closed_terms with
 	  Some flags ->
 	    is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
-	| None -> eq_constr m n)
+	| None -> constr_cmp (conv_pb_of cv_pb) m n)
     then 
       subst
     else