Quote: replaced various generic = on constr by eq_constr, destructors etc.

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

1 files changed, 12 insertions, 7 deletions

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index a81392ad4..fbb754204 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -166,7 +166,7 @@ exchange ?1 and ?2 in the example above)
 module ConstrSet = Set.Make(
   struct
     type t = constr
-    let compare = (Pervasives.compare : t->t->int)
+    let compare = constr_ord
   end)
 
 type inversion_scheme = {
@@ -208,7 +208,7 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c =
     match kind_of_term c with
-      | App (j, args) when j = mkRel (index_of_f) (* recursive call *) ->
+      | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) ->
           let i = destRel (array_last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
@@ -240,7 +240,7 @@ let compute_ivs gl f cs =
            (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *)
            (* REL 1 to REL nargsi are argsi (reverse order) *)
            (* First we test if the RHS is the RHS for constants *)
-                   if bodyi = mkRel 1 then
+                   if isRel bodyi && destRel bodyi = 1 then
                      c_lhs := Some (compute_lhs (snd (List.hd args3))
                                       i nargsi)
            (* Then we test if the RHS is the RHS for variables *)
@@ -377,6 +377,12 @@ let rec sort_subterm gl l =
     | [] -> []
     | h::t -> insert h (sort_subterm gl t)
 
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
 (*s Now we are able to do the inversion itself.
   We destructurate the term and use an imperative hashtable
   to store leafs that are already encountered.
@@ -384,10 +390,9 @@ let rec sort_subterm gl l =
   [ivs : inversion_scheme]\\
   [lc: constr list]\\
   [gl: goal sigma]\\ *)
-
 let quote_terms ivs lc gl =
   Coqlib.check_required_library ["Coq";"quote";"Quote"];
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
   let varlist = ref ([] : constr list) in (* list of variables *)
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c =
@@ -414,7 +419,7 @@ let quote_terms ivs lc gl =
 			 Termops.subst_meta [1, c] c_lhs
                      | _ ->
 			 begin
-                           try Hashtbl.find varhash c
+                           try Constrhash.find varhash c
                            with Not_found ->
                              let newvar =
                                Termops.subst_meta [1, (path_of_int !counter)]
@@ -422,7 +427,7 @@ let quote_terms ivs lc gl =
                              begin
                                incr counter;
                                varlist := c :: !varlist;
-                               Hashtbl.add varhash c newvar;
+                               Constrhash.add varhash c newvar;
                                newvar
                              end
 			 end