Make eq_pattern_test/eq_test work up to the equivalence of primitive

projections with their eta-expanded constant form.

2 files changed, 37 insertions, 0 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 232573d5f0..7fe4258c2d 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -215,6 +215,39 @@ let leq_constr_universes m n =
     let res = compare_leq m n in
       res, !cstrs
 
+let compare_head_gen_proj env equ eqs eqc' m n =
+  match kind_of_term m, kind_of_term n with
+  | Proj (p, c), App (f, args)
+  | App (f, args), Proj (p, c) -> 
+    (match kind_of_term f with
+    | Const (p', u) when eq_constant p p' -> 
+      let pb = Environ.lookup_projection p env in
+      let npars = pb.Declarations.proj_npars in
+	if Array.length args == npars + 1 then
+	  eqc' c args.(npars)
+	else false
+    | _ -> false)
+  | _ -> Constr.compare_head_gen equ eqs eqc' m n
+    
+let eq_constr_universes_proj env m n =
+  if m == n then true, Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+	 true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
+    in
+    let res = eq_constr' m n in
+      res, !cstrs
+
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
   RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
diff --git a/library/universes.mli b/library/universes.mli
index 6cfee48d24..e4bb218336 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -80,6 +80,10 @@ val eq_constr_universes : constr -> constr -> bool universe_constrained
     alpha, casts, application grouping and the universe constraints in [c]. *)
 val leq_constr_universes : constr -> constr -> bool universe_constrained
 
+(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
+    application grouping and the universe constraints in [c]. *)
+val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
+
 (** Build a fresh instance for a given context, its associated substitution and 
     the instantiated constraints. *)