Imported Upstream version 8.4~betaupstream/8.4_beta

13 files changed, 27 insertions, 140 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 1f3fd595..d67dceea 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.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: formula.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Hipattern
 open Names
 open Term
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index a831c087..379aaff1 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -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: formula.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 open Names
 open Libnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8e68506c..4a38c48d 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  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        *)
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma"  i*)
 
-(* $Id: g_ground.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Formula
 open Sequent
 open Ground
@@ -29,6 +27,7 @@ let ground_depth=ref 3
 let _=
   let gdopt=
     { optsync=true;
+      optdepr=false;
       optname="Firstorder Depth";
       optkey=["Firstorder";"Depth"];
       optread=(fun ()->Some !ground_depth);
@@ -44,6 +43,7 @@ let congruence_depth=ref 100
 let _=
   let gdopt=
     { optsync=true;
+      optdepr=false;
       optname="Congruence Depth";
       optkey=["Congruence";"Depth"];
       optread=(fun ()->Some !congruence_depth);
@@ -111,7 +111,6 @@ let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_loc
 let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global
 
 ARGUMENT EXTEND firstorder_using
-  TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
   RAW_TYPED AS reference_list
   RAW_PRINTED BY pr_firstorder_using_raw
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 163b9891..46708053 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.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: ground.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Formula
 open Sequent
 open Rules
@@ -18,32 +16,6 @@ open Tactics
 open Tacticals
 open Libnames
 
-(*
-let old_search=ref !Auto.searchtable
-
-(* I use this solution as a means to know whether hints have changed,
-but this prevents the GC from collecting the previous table,
-resulting in some limited space wasting*)
-
-let update_flags ()=
-  if not ( !Auto.searchtable == !old_search ) then
-    begin
-      old_search:=!Auto.searchtable;
-      let predref=ref Names.KNpred.empty in
-      let f p_a_t =
-	match p_a_t.Auto.code with
-	    Auto.Unfold_nth (ConstRef kn)->
-	      predref:=Names.KNpred.add kn !predref
-	  | _ ->() in
-      let g _ l=List.iter f l in
-      let h _ hdb=Auto.Hint_db.iter g hdb in
-	Util.Stringmap.iter h !Auto.searchtable;
-	red_flags:=
-	Closure.RedFlags.red_add_transparent
-	  Closure.betaiotazeta (Names.Idpred.full,!predref)
-    end
-*)
-
 let update_flags ()=
   let predref=ref Names.Cpred.empty in
   let f coe=
@@ -61,7 +33,7 @@ let ground_tac solver startseq gl=
   update_flags ();
   let rec toptac skipped seq gl=
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
-    then Pp.msgnl (Printer.pr_goal (sig_it gl));
+    then Pp.msgnl (Printer.pr_goal gl);
     tclORELSE (axiom_tac seq.gl seq)
       begin
 	try
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 8328bb3a..a4ee68fd 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -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: ground.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 val ground_tac:     Tacmach.tactic ->
   (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 4802aaa3..16831d3e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,20 +1,18 @@
 (************************************************************************)
 (*  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        *)
 (************************************************************************)
 
-(*i $Id: instances.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Formula
 open Sequent
 open Unify
 open Rules
 open Util
 open Term
-open Rawterm
+open Glob_term
 open Tacmach
 open Tactics
 open Tacticals
@@ -35,11 +33,11 @@ let compare_instance inst1 inst2=
 	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
 	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
 
-let compare_gr id1 id2=
+let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else Pervasives.compare id1 id2
+    else Libnames.RefOrdered.compare id1 id2
 
 module OrderedInstance=
 struct
@@ -125,9 +123,9 @@ let mk_open_instance id gl m t=
   let rec raux n t=
     if n=0 then t else
       match t with
-	  RLambda(loc,name,k,_,t0)->
+	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
-	      RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1)
+	      GLambda(loc,name,k,GHole (dummy_loc,Evd.BinderType name),t1)
 	| _-> anomaly "can't happen" in
   let ntt=try
     Pretyping.Default.understand evmap env (raux m rawt)
@@ -181,12 +179,12 @@ let right_instance_tac inst continue seq=
 	[tclTHENLIST
 	   [introf;
 	    (fun gls->
-	       split (Rawterm.ImplicitBindings
+	       split (Glob_term.ImplicitBindings
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	(tclTHEN (split (Glob_term.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 537e40e7..be69b067 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -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        *)
 (************************************************************************)
 
-(*i $Id: instances.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Term
 open Tacmach
 open Names
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index e6d73fb6..23eeb2f6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.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: rules.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Util
 open Names
 open Term
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index a5a6b614..7d1e57f4 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -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: rules.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 open Tacmach
 open Names
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
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index ef052605..c5c2bb95 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -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.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 open Util
 open Formula
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 4e0ad108..299a0054 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.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        *)
 (************************************************************************)
 
-(*i $Id: unify.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Util
 open Formula
 open Tacmach
@@ -91,9 +89,8 @@ let unif t1 t2=
 let value i t=
   let add x y=
     if x<0 then y else if y<0 then x else x+y in
-  let tref=mkMeta i in
   let rec vaux term=
-    if term=tref then 0 else
+    if isMeta term && destMeta term = i then 0 else
       let f v t=add v (vaux t) in
       let vr=fold_constr f (-1) term in
 	if vr<0 then -1 else vr+1 in
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 4e0d88d3..06865611 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -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: unify.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Term
 
 exception UFAIL of constr*constr