From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 plugins/firstorder/sequent.ml | 71 +++----------------------------------------
 1 file changed, 4 insertions(+), 67 deletions(-)

(limited to 'plugins/firstorder/sequent.ml')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index faac286e..f75678c6 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: sequent.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 open Util
 open Formula
@@ -59,71 +57,10 @@ struct
 	(priority e1.pat) - (priority e2.pat)
 end
 
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let rec compare_list f l1 l2=
-  match l1,l2 with
-      [],[]-> 0
-    | [],_ -> -1
-    | _,[] -> 1
-    | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
-
-let compare_array f v1 v2=
-  let l=Array.length v1 in
-  let c=l - Array.length v2 in
-    if c=0 then
-      let rec comp_aux i=
-	if i<0 then 0
-	else
-	  let ci=f v1.(i) v2.(i) in
-	    if ci=0 then
-	      comp_aux (i-1)
-	    else ci
-      in comp_aux (l-1)
-    else c
-
-let compare_constr_int f t1 t2 =
-  match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> n1 - n2
-    | Meta m1, Meta m2 -> m1 - m2
-    | Var id1, Var id2 -> Pervasives.compare id1 id2
-    | Sort s1, Sort s2 -> Pervasives.compare s1 s2
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
-    | Prod (_,t1,c1), Prod (_,t2,c2)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	(f =? f) t1 t2 c1 c2
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
-    | App (_,_), App (_,_) ->
-	let c1,l1=decompose_app t1
-	and c2,l2=decompose_app t2 in
-	  (f =? (compare_list f)) c1 c2 l1 l2
-    | Evar (e1,l1), Evar (e2,l2) ->
-	((-) =? (compare_array f)) e1 e2 l1 l2
-    | Const c1, Const c2 -> Pervasives.compare c1 c2
-    | Ind c1, Ind c2 -> Pervasives.compare c1 c2
-    | Construct c1, Construct c2 -> Pervasives.compare c1 c2
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	((f =? f) ==? (compare_array f)) p1 p2 c1 c2 bl1 bl2
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	((Pervasives.compare =? (compare_array f)) ==? (compare_array f))
-	ln1 ln2 tl1 tl2 bl1 bl2
-    | _ -> Pervasives.compare t1 t2
-
-let rec compare_constr m n=
-  compare_constr_int compare_constr m n
-
 module OrderedConstr=
 struct
   type t=constr
-  let compare=compare_constr
+  let compare=constr_ord
 end
 
 type h_item = global_reference * (int*constr) option
@@ -132,7 +69,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare
+    (Libnames.RefOrdered.compare
      =? (fun oc1 oc2 ->
 	   match oc1,oc2 with
 	       Some (m1,c1),Some (m2,c2) ->
@@ -283,7 +220,7 @@ let extend_with_auto_hints l seq gl=
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-  let g _ l=List.iter f l in
+  let g _ l = List.iter f l in
   let h dbname=
     let hdb=
       try
-- 
cgit v1.2.3