Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

13 files changed, 0 insertions, 1676 deletions

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
deleted file mode 100644
index 0be468aa..00000000
--- a/contrib/first-order/formula.ml
+++ /dev/null
@@ -1,270 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: formula.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
-
-open Hipattern
-open Names
-open Term
-open Termops
-open Reductionops
-open Tacmach
-open Util
-open Declarations
-open Libnames
-open Inductiveops
-
-let qflag=ref true
-
-let red_flags=ref Closure.betaiotazeta
-
-let (=?) f g i1 i2 j1 j2=
-  let c=f i1 i2 in
-    if c=0 then g j1 j2 else c
-
-let (==?) fg h i1 i2 j1 j2 k1 k2=
-  let c=fg i1 i2 j1 j2 in
-    if c=0 then h k1 k2 else c
-
-type ('a,'b) sum = Left of 'a | Right of 'b
-
-type counter = bool -> metavariable
-
-exception Is_atom of constr
-
-let meta_succ m = m+1
-
-let rec nb_prod_after n c=
-  match kind_of_term c with
-    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
-	1+(nb_prod_after 0 b)
-    | _ -> 0
-
-let construct_nhyps ind gls =
-  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
-  let hyp = nb_prod_after nparams in	
-    Array.map hyp constr_types
-
-(* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
-let ind_hyps nevar ind largs gls= 
-  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in 
-  let lp=Array.length types in     
-  let myhyps i=
-    let t1=Term.prod_applist types.(i) largs in
-    let t2=snd (Sign.decompose_prod_n_assum nevar t1) in
-      fst (Sign.decompose_prod_assum t2) in
-    Array.init lp myhyps
-
-let special_nf gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
-
-let special_whd gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
-
-type kind_of_formula=
-    Arrow of constr*constr
-  | False of inductive*constr list
-  | And of inductive*constr list*bool
-  | Or of inductive*constr list*bool
-  | Exists of inductive*constr list
-  | Forall of constr*constr
-  | Atom of constr
-      
-let rec kind_of_formula gl term =
-  let normalize=special_nf gl in
-  let cciterm=special_whd gl term in
-    match match_with_imp_term cciterm with
-	Some (a,b)-> Arrow(a,(pop b))
-      |_->
-	 match match_with_forall_term cciterm with
-	     Some (_,a,b)-> Forall(a,b)
-	   |_-> 
-	      match match_with_nodep_ind cciterm with
-		  Some (i,l,n)->
-		    let ind=destInd i in
-		    let (mib,mip) = Global.lookup_inductive ind in
-		    let nconstr=Array.length mip.mind_consnames in
-		      if nconstr=0 then 
-			False(ind,l)
-		      else
-			let has_realargs=(n>0) in
-			let is_trivial=
-			  let is_constant c =
-			    nb_prod c = mib.mind_nparams in  
-			    array_exists is_constant mip.mind_nf_lc in 
-			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
-			    (has_realargs && not is_trivial)
-			  then
-			    Atom cciterm 
-			  else
-			    if nconstr=1 then
-			      And(ind,l,is_trivial)
-			    else 
-			      Or(ind,l,is_trivial) 
-		| _ ->  
-		    match match_with_sigma_type cciterm with
-			Some (i,l)-> Exists((destInd i),l)
-		      |_-> Atom (normalize cciterm)
-  
-type atoms = {positive:constr list;negative:constr list}
-
-type side = Hyp | Concl | Hint
-
-let no_atoms = (false,{positive=[];negative=[]})
-
-let dummy_id=VarRef (id_of_string "")
-
-let build_atoms gl metagen side cciterm =
-  let trivial =ref false
-  and positive=ref []
-  and negative=ref [] in
-  let normalize=special_nf gl in 
-  let rec build_rec env polarity cciterm=
-    match kind_of_formula gl cciterm with
-	False(_,_)->if not polarity then trivial:=true
-      | Arrow (a,b)->
-	  build_rec env (not polarity) a;
-	  build_rec env polarity b
-      | And(i,l,b) | Or(i,l,b)->
-	  if b then 
-	    begin
-	      let unsigned=normalize (substnl env 0 cciterm) in
-		if polarity then 
-		  positive:= unsigned :: !positive 
-		else 
-		  negative:= unsigned :: !negative
-	    end;
-	  let v = ind_hyps 0 i l gl in
-	  let g i _ (_,_,t) =
-	    build_rec env polarity (lift i t) in
-	  let f l =
-	    list_fold_left_i g (1-(List.length l)) () l in
-	    if polarity && (* we have a constant constructor *)
-	      array_exists (function []->true|_->false) v 
-	    then trivial:=true;
-	    Array.iter f v 
-      | Exists(i,l)->
-	  let var=mkMeta (metagen true) in
-	  let v =(ind_hyps 1 i l gl).(0) in
-	  let g i _ (_,_,t) =
-	    build_rec (var::env) polarity (lift i t) in
-	    list_fold_left_i g (2-(List.length l)) () v
-      | Forall(_,b)->
-	  let var=mkMeta (metagen true) in
-	    build_rec (var::env) polarity b
-      | Atom t->
-	  let unsigned=substnl env 0 t in
-	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
-	      if polarity then 
-		positive:= unsigned :: !positive 
-	      else 
-		negative:= unsigned :: !negative in
-    begin
-      match side with
-	  Concl    -> build_rec [] true cciterm
-	| Hyp      -> build_rec [] false cciterm
-	| Hint     -> 
-	    let rels,head=decompose_prod cciterm in
-	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
-	      build_rec env false head;trivial:=false (* special for hints *)
-    end;
-    (!trivial,
-     {positive= !positive;
-      negative= !negative})
-    
-type right_pattern =
-    Rarrow
-  | Rand
-  | Ror 
-  | Rfalse
-  | Rforall
-  | Rexists of metavariable*constr*bool
-   
-type left_arrow_pattern=
-    LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
-  | LLforall of constr
-  | LLexists of inductive*constr list
-  | LLarrow of constr*constr*constr
-
-type left_pattern=
-    Lfalse    
-  | Land of inductive
-  | Lor of inductive 
-  | Lforall of metavariable*constr*bool
-  | Lexists of inductive
-  | LA of constr*left_arrow_pattern
-
-type t={id:global_reference;
-	constr:constr;
-	pat:(left_pattern,right_pattern) sum;
-	atoms:atoms}
-    
-let build_formula side nam typ gl metagen=
-  let normalize = special_nf gl in
-    try 
-      let m=meta_succ(metagen false) in
-      let trivial,atoms=
-	if !qflag then 
-	  build_atoms gl metagen side typ 
-	else no_atoms in
-      let pattern=
-	match side with
-	    Concl ->
-	      let pat=
-		match kind_of_formula gl typ with
-		    False(_,_)        -> Rfalse
-		  | Atom a       -> raise (Is_atom a)
-		  | And(_,_,_)        -> Rand
-		  | Or(_,_,_)         -> Ror
-		  | Exists (i,l) -> 
-		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
-			Rexists(m,d,trivial)
-		  | Forall (_,a) -> Rforall 
-		  | Arrow (a,b) -> Rarrow in
-		Right pat
-	  | _ ->
-	      let pat=
-		match kind_of_formula gl typ with
-		    False(i,_)        ->  Lfalse
-		  | Atom a       ->  raise (Is_atom a)
-		  | And(i,_,b)         ->  
-		      if b then
-			let nftyp=normalize typ in raise (Is_atom nftyp)
-		      else Land i
-		  | Or(i,_,b)          ->
-		      if b then
-			let nftyp=normalize typ in raise (Is_atom nftyp)
-		      else Lor i
-		  | Exists (ind,_) ->  Lexists ind 
-		  | Forall (d,_) -> 
-		      Lforall(m,d,trivial)
-		  | Arrow (a,b) ->
-		      let nfa=normalize a in
-			LA (nfa, 
-			    match kind_of_formula gl a with
-				False(i,l)-> LLfalse(i,l)
-			      | Atom t->     LLatom
-			      | And(i,l,_)-> LLand(i,l)
-			      | Or(i,l,_)->  LLor(i,l)
-			      | Arrow(a,c)-> LLarrow(a,c,b)
-			      | Exists(i,l)->LLexists(i,l)
-			      | Forall(_,_)->LLforall a) in
-		Left pat
-      in
-	Left {id=nam;
-	      constr=normalize typ;
-	      pat=pattern;
-	      atoms=atoms}
-    with Is_atom a-> Right a (* already in nf *)
-
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
deleted file mode 100644
index 8703045c..00000000
--- a/contrib/first-order/formula.mli
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: formula.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-open Term
-open Names
-open Libnames
-
-val qflag : bool ref
-
-val red_flags: Closure.RedFlags.reds ref
-
-val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
-  'a -> 'a -> 'b -> 'b -> int
-  
-val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
-  'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
-
-type ('a,'b) sum = Left of 'a | Right of 'b
-
-type counter = bool -> metavariable
-
-val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
-
-val ind_hyps : int -> inductive -> constr list -> 
-  Proof_type.goal Tacmach.sigma -> Sign.rel_context array
-
-type atoms = {positive:constr list;negative:constr list}
-
-type side = Hyp | Concl | Hint
-
-val dummy_id: global_reference
-			
-val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
-  side -> constr -> bool * atoms
-
-type right_pattern =
-    Rarrow
-  | Rand
-  | Ror 
-  | Rfalse
-  | Rforall
-  | Rexists of metavariable*constr*bool
-    
-type left_arrow_pattern=
-    LLatom
-  | LLfalse of inductive*constr list
-  | LLand of inductive*constr list
-  | LLor of inductive*constr list
-  | LLforall of constr
-  | LLexists of inductive*constr list
-  | LLarrow of constr*constr*constr
-
-type left_pattern=
-    Lfalse    
-  | Land of inductive
-  | Lor of inductive 
-  | Lforall of metavariable*constr*bool
-  | Lexists of inductive
-  | LA of constr*left_arrow_pattern
-      
-type t={id: global_reference;
-	constr: constr;
-	pat: (left_pattern,right_pattern) sum;
-	atoms: atoms}
-    
-(*exception Is_atom of constr*)
-
-val build_formula : side -> global_reference -> types -> 
-  Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
-
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
deleted file mode 100644
index 366f563b..00000000
--- a/contrib/first-order/g_ground.ml4
+++ /dev/null
@@ -1,127 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "parsing/grammar.cma"  i*)
-
-(* $Id: g_ground.ml4 9154 2006-09-20 17:18:18Z corbinea $ *)
-
-open Formula
-open Sequent
-open Ground
-open Goptions
-open Tactics
-open Tacticals
-open Tacinterp
-open Term
-open Names
-open Util
-open Libnames
-
-(* declaring search depth as a global option *)
-
-let ground_depth=ref 3
-
-let _=
-  let gdopt=
-    { optsync=true;
-      optname="Firstorder Depth";
-      optkey=SecondaryTable("Firstorder","Depth"); 
-      optread=(fun ()->Some !ground_depth); 
-      optwrite=
-   (function 
-	None->ground_depth:=3
-      |	Some i->ground_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
-let congruence_depth=ref 100
-
-let _=
-  let gdopt=
-    { optsync=true;
-      optname="Congruence Depth";
-      optkey=SecondaryTable("Congruence","Depth"); 
-      optread=(fun ()->Some !congruence_depth); 
-      optwrite=
-   (function 
-	None->congruence_depth:=0
-      |	Some i->congruence_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
-let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
-
-let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
-		      
-type external_env=
-    Ids of global_reference list
-  | Bases of Auto.hint_db_name list
-  | Void
-
-let gen_ground_tac flag taco ext gl=
-  let backup= !qflag in
-    try
-      qflag:=flag;
-      let solver= 
-	match taco with 
-	    Some tac-> tac
-	  | None-> default_solver in
-      let startseq=
-	match ext with
-	    Void -> (fun gl -> empty_seq !ground_depth)
-	  | Ids l-> create_with_ref_list l !ground_depth
-	  | Bases l-> create_with_auto_hints l !ground_depth in
-      let result=ground_tac solver startseq gl in 
-	qflag:=backup;result
-    with e ->qflag:=backup;raise e
-      
-(* special for compatibility with Intuition 
-
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
-
-let defined_connectives=lazy
-  [[],EvalConstRef (destConst (constant "not"));
-   [],EvalConstRef (destConst (constant "iff"))]
-
-let normalize_evaluables=
-  onAllClauses
-    (function 
-	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some id-> 
-	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (Tacexpr.InHypType id)) *)
-
-TACTIC EXTEND firstorder
-    [ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ]
-|   [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) (Bases l) ]
-|   [ "firstorder" tactic_opt(t) ] -> 
-      [ gen_ground_tac true (option_map eval_tactic t) Void ]
-END
-
-TACTIC EXTEND gintuition
-  [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (option_map eval_tactic t) Void ]
-END
-
-
-let default_declarative_automation gls = 
-  tclORELSE 
-    (Cctac.congruence_tac !congruence_depth []) 
-    (gen_ground_tac true 
-       (Some (tclTHEN
-		default_solver
-		(Cctac.congruence_tac !congruence_depth [])))
-       Void) gls
-
-
-
-let () = 
-  Decl_proof_instr.register_automation_tac default_declarative_automation
-
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
deleted file mode 100644
index bccac6df..00000000
--- a/contrib/first-order/ground.ml
+++ /dev/null
@@ -1,152 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: ground.ml 9537 2007-01-26 10:05:04Z corbinea $ *)
-
-open Formula
-open Sequent
-open Rules
-open Instances
-open Term
-open Tacmach
-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=
-    try
-      let kn=destConst (Classops.get_coercion_value coe) in
-	predref:=Names.Cpred.add kn !predref
-    with Invalid_argument "destConst"-> () in
-    List.iter f (Classops.coercions ());
-    red_flags:=
-    Closure.RedFlags.red_add_transparent 
-      Closure.betaiotazeta 
-      (Names.Idpred.full,Names.Cpred.complement !predref)
-
-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));
-    tclORELSE (axiom_tac seq.gl seq)
-      begin
-	try      
-	  let (hd,seq1)=take_formula seq  
-	  and re_add s=re_add_formula_list skipped s in
-	  let continue=toptac [] 
-	  and backtrack gl=toptac (hd::skipped) seq1 gl in
-	    match hd.pat with
-		Right rpat->
-		  begin
-		    match rpat with
-			Rand->
-			  and_tac backtrack continue (re_add seq1)
-		      | Rforall->
-			  let backtrack1=
-			    if !qflag then 
-			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
-			    else
-			      backtrack in
-			    forall_tac backtrack1 continue (re_add seq1)
-		      | Rarrow->
-			  arrow_tac backtrack continue (re_add seq1)
-		      | Ror->
-			  or_tac  backtrack continue (re_add seq1)
-		      | Rfalse->backtrack 
-		      | Rexists(i,dom,triv)->
-			  let (lfp,seq2)=collect_quantified seq in
-			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
-				continue (re_add seq)
-			    else
-			      backtrack2 (* need special backtracking *)
-		  end
-	      | Left lpat->
-		  begin
-		    match lpat with
-			Lfalse->
-			  left_false_tac hd.id
-		      | Land ind->
-			  left_and_tac ind backtrack 
-			  hd.id continue (re_add seq1)
-		      | Lor ind->
-			  left_or_tac ind backtrack 
-			  hd.id continue (re_add seq1)
-		      | Lforall (_,_,_)->
-			  let (lfp,seq2)=collect_quantified seq in
-			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
-				continue (re_add seq)
-			    else
-			      backtrack2 (* need special backtracking *)
-  		      | Lexists ind ->
-			  if !qflag then 
-			    left_exists_tac ind backtrack hd.id
-			      continue (re_add seq1)
-			  else backtrack
-		      | LA (typ,lap)->
-			  let la_tac=
-			    begin
-			      match lap with
-				  LLatom -> backtrack 
-				| LLand (ind,largs) | LLor(ind,largs) 
-				| LLfalse (ind,largs)->
-				    (ll_ind_tac ind largs backtrack 
-				       hd.id continue (re_add seq1)) 
-				| LLforall p ->	      
-				    if seq.depth>0 && !qflag then 
-				      (ll_forall_tac p backtrack 
-					 hd.id continue (re_add seq1))
-				    else backtrack
-				| LLexists (ind,l) ->
-				    if !qflag then
-				      ll_ind_tac ind l backtrack
-					hd.id continue (re_add seq1)
-				    else
-				      backtrack
-				| LLarrow (a,b,c) ->	      
-				    (ll_arrow_tac a b c backtrack
-				       hd.id continue (re_add seq1))
-			    end in			 
-			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
-		  end
-	    with Heap.EmptyHeap->solver
-      end gl in
-    wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
-      
diff --git a/contrib/first-order/ground.mli b/contrib/first-order/ground.mli
deleted file mode 100644
index 621f99db..00000000
--- a/contrib/first-order/ground.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: ground.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-val ground_tac:     Tacmach.tactic ->
-  (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
-
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
deleted file mode 100644
index 254d7b84..00000000
--- a/contrib/first-order/instances.ml
+++ /dev/null
@@ -1,206 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: instances.ml 8654 2006-03-22 15:36:58Z msozeau $ i*)
-
-open Formula
-open Sequent
-open Unify
-open Rules
-open Util
-open Term
-open Rawterm
-open Tacmach
-open Tactics
-open Tacticals
-open Termops
-open Reductionops
-open Declarations
-open Formula
-open Sequent
-open Names
-open Libnames
-
-let compare_instance inst1 inst2=
-	match inst1,inst2 with
-	    Phantom(d1),Phantom(d2)->
-	      (OrderedConstr.compare d1 d2)
-	  | Real((m1,c1),n1),Real((m2,c2),n2)->
-	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
-	  | 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=
-  if id1==id2 then 0 else
-    if id1==dummy_id then 1 
-    else if id2==dummy_id then -1 
-    else Pervasives.compare id1 id2
-
-module OrderedInstance=
-struct
-  type t=instance * Libnames.global_reference
-  let compare (inst1,id1) (inst2,id2)=
-    (compare_instance =? compare_gr) inst2 inst1 id2 id1
-    (* we want a __decreasing__ total order *)
-end
-  
-module IS=Set.Make(OrderedInstance)
-
-let make_simple_atoms seq=
-  let ratoms=
-    match seq.glatom with
-	Some t->[t]
-      | None->[]
-  in {negative=seq.latoms;positive=ratoms}
-
-let do_sequent setref triv id seq i dom atoms=
-  let flag=ref true in
-  let phref=ref triv in
-  let do_atoms a1 a2 =
-    let do_pair t1 t2 = 
-      match unif_atoms i dom t1 t2 with
-	  None->()
-	| Some (Phantom _) ->phref:=true
-	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
-      List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
-      List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
-    HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
-    do_atoms atoms (make_simple_atoms seq);
-    !flag && !phref 
- 
-let match_one_quantified_hyp setref seq lf=
-  match lf.pat with 
-      Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-	if do_sequent setref triv lf.id seq i dom lf.atoms then
-	  setref:=IS.add ((Phantom dom),lf.id) !setref 
-    | _ ->anomaly "can't happen" 
-
-let give_instances lf seq=
-  let setref=ref IS.empty in
-    List.iter (match_one_quantified_hyp setref seq) lf;
-    IS.elements !setref
-	  	  
-(* collector for the engine *)
-
-let rec collect_quantified seq=
-  try
-    let hd,seq1=take_formula seq in
-      (match hd.pat with 
-	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> 
-	     let (q,seq2)=collect_quantified seq1 in
-	       ((hd::q),seq2)
-	 | _->[],seq)
-  with Heap.EmptyHeap -> [],seq
-
-(* open instances processor *)
-
-let dummy_constr=mkMeta (-1)
-
-let dummy_bvid=id_of_string "x"
-
-let mk_open_instance id gl m t=
-  let env=pf_env gl in
-  let evmap=Refiner.project gl in
-  let var_id=
-    if id==dummy_id then dummy_bvid else
-      let typ=pf_type_of gl (constr_of_global id) in
-	(* since we know we will get a product, 
-	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
-	match nam with 
-	    Name id -> id
-	  | Anonymous ->  dummy_bvid in
-  let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
-  let rec aux n avoid=
-    if n=0 then [] else
-      let nid=(fresh_id avoid var_id gl) in
-	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
-  let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] nt in
-  let rec raux n t=
-    if n=0 then t else 
-      match t with
-	  RLambda(loc,name,_,t0)->
-	    let t1=raux (n-1) t0 in
-	      RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1)
-	| _-> anomaly "can't happen" in
-  let ntt=try 
-    Pretyping.Default.understand evmap env (raux m rawt)
-  with _ -> 
-    error "Untypable instance, maybe higher-order non-prenex quantification" in
-    Sign.decompose_lam_n_assum m ntt
-
-(* tactics   *)
-
-let left_instance_tac (inst,id) continue seq=
-  match inst with
-      Phantom dom->
-	if lookup (id,None) seq then 
-	  tclFAIL 0 (Pp.str "already done")
-	else
-	  tclTHENS (cut dom) 
-	    [tclTHENLIST
-	       [introf;
-		(fun gls->generalize 
-		   [mkApp(constr_of_global id,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
-		introf;
-		tclSOLVE [wrap 1 false continue 
-			    (deepen (record (id,None) seq))]];
-	    tclTRY assumption]
-    | Real((m,t) as c,_)->
-	if lookup (id,Some c) seq then 
-	  tclFAIL 0 (Pp.str "already done")
-	else 
-	  let special_generalize=
-	    if m>0 then 
-	      fun gl-> 
-		let (rc,ot)= mk_open_instance id gl m t in
-		let gt= 
-		  it_mkLambda_or_LetIn 
-		    (mkApp(constr_of_global id,[|ot|])) rc in
-		  generalize [gt] gl
-	    else
-	      generalize [mkApp(constr_of_global id,[|t|])]
-	  in
-	    tclTHENLIST 
-	      [special_generalize;
-	       introf; 
-	       tclSOLVE 
-		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
-	      
-let right_instance_tac inst continue seq=
-  match inst with
-      Phantom dom ->
-	tclTHENS (cut dom) 
-	[tclTHENLIST
-	   [introf;
-	    (fun gls->
-	       split (Rawterm.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]))
-	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
-    | Real ((m,t),_) ->
-	tclFAIL 0 (Pp.str "not implemented ... yet")
-
-let instance_tac inst=
-  if (snd inst)==dummy_id then 
-    right_instance_tac (fst inst)
-  else
-    left_instance_tac inst
-
-let quantified_tac lf backtrack continue seq gl=
-  let insts=give_instances lf seq in
-    tclORELSE
-      (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
-      backtrack gl
-
- 
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
deleted file mode 100644
index 7667c89f..00000000
--- a/contrib/first-order/instances.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: instances.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
-
-open Term
-open Tacmach
-open Names
-open Libnames
-open Rules
-  
-val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
-
-val give_instances : Formula.t list -> Sequent.t -> 
-  (Unify.instance * global_reference) list
-
-val quantified_tac : Formula.t list -> seqtac with_backtracking
-
-
-
-
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
deleted file mode 100644
index 6c51eda3..00000000
--- a/contrib/first-order/rules.ml
+++ /dev/null
@@ -1,216 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: rules.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
-
-open Util
-open Names
-open Term
-open Tacmach
-open Tactics
-open Tacticals
-open Termops
-open Declarations
-open Formula
-open Sequent
-open Libnames
-
-type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
-
-type lseqtac= global_reference -> seqtac
-
-type 'a with_backtracking = tactic -> 'a
-
-let wrap n b continue seq gls=
-  check_for_interrupt ();
-  let nc=pf_hyps gls in
-  let env=pf_env gls in
-  let rec aux i nc ctx=
-    if i<=0 then seq else 
-      match nc with
-	  []->anomaly "Not the expected number of hyps"
-	| ((id,_,typ) as nd)::q->  
-	    if occur_var env id (pf_concl gls) || 
-	      List.exists (occur_var_in_decl env id) ctx then
-		(aux (i-1) q (nd::ctx))
-	    else
-	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
-  let seq1=aux n nc [] in
-  let seq2=if b then 
-    add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
-    continue seq2 gls
-
-let id_of_global=function
-    VarRef id->id
-  | _->assert false
-
-let clear_global=function
-    VarRef id->clear [id]
-  | _->tclIDTAC
-      
-
-(* connection rules *)
-
-let axiom_tac t seq=
-  try exact_no_check (constr_of_global (find_left t seq)) 
-  with Not_found->tclFAIL 0 (Pp.str "No axiom link")
-
-let ll_atom_tac a backtrack id continue seq= 
-  tclIFTHENELSE
-    (try 
-      tclTHENLIST
-	[generalize [mkApp(constr_of_global id,
-			   [|constr_of_global (find_left a seq)|])];
-	 clear_global id;
-	 intro]
-    with Not_found->tclFAIL 0 (Pp.str "No link"))
-    (wrap 1 false continue seq) backtrack 
-
-(* right connectives rules *)
-
-let and_tac backtrack continue seq=
-  tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
-
-let or_tac backtrack continue seq=
-  tclORELSE 
-    (any_constructor (Some (tclCOMPLETE (wrap 0 true continue seq))))
-    backtrack
-
-let arrow_tac backtrack continue seq=
-  tclIFTHENELSE intro (wrap 1 true continue seq)
-    (tclORELSE
-       (tclTHEN introf (tclCOMPLETE (wrap 1 true continue seq)))
-       backtrack)
-(* left connectives rules *)
-
-let left_and_tac ind backtrack id continue seq gls=
- let n=(construct_nhyps ind gls).(0) in  
-   tclIFTHENELSE
-     (tclTHENLIST 
-      [simplest_elim (constr_of_global id);
-       clear_global id; 
-       tclDO n intro])
-     (wrap n false continue seq)
-     backtrack gls
-
-let left_or_tac ind backtrack id continue seq gls=
-  let v=construct_nhyps ind gls in  
-  let f n=
-    tclTHENLIST
-      [clear_global id;
-       tclDO n intro;
-       wrap n false continue seq] in
-    tclIFTHENSVELSE
-      (simplest_elim (constr_of_global id))
-      (Array.map f v)
-      backtrack gls
-
-let left_false_tac id=
-  simplest_elim (constr_of_global id)
-
-(* left arrow connective rules *)
-
-(* We use this function for false, and, or, exists *)
-
-let ll_ind_tac ind largs backtrack id continue seq gl= 
-     let rcs=ind_hyps 0 ind largs gl in
-     let vargs=Array.of_list largs in
-	     (* construire le terme  H->B, le generaliser etc *)   
-     let myterm i=
-       let rc=rcs.(i) in
-       let p=List.length rc in
-       let cstr=mkApp ((mkConstruct (ind,(i+1))),vargs) in
-       let vars=Array.init p (fun j->mkRel (p-j)) in
-       let capply=mkApp ((lift p cstr),vars) in
-       let head=mkApp ((lift p (constr_of_global id)),[|capply|]) in
-	 Sign.it_mkLambda_or_LetIn head rc in
-       let lp=Array.length rcs in
-       let newhyps=list_tabulate myterm lp in
-	 tclIFTHENELSE
-	   (tclTHENLIST 
-	      [generalize newhyps;
-	       clear_global id;
-	       tclDO lp intro])
-	   (wrap lp false continue seq) backtrack gl
-
-let ll_arrow_tac a b c backtrack id continue seq=
-  let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d=mkLambda (Anonymous,b,
-		  mkApp ((constr_of_global id),
-			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
-    tclORELSE
-      (tclTHENS (cut c)
-	 [tclTHENLIST
-	    [introf;
-	     clear_global id;
-	     wrap 1 false continue seq];
-	  tclTHENS (cut cc) 
-            [exact_no_check (constr_of_global id); 
-	     tclTHENLIST 
-	       [generalize [d];
-		clear_global id;
-		introf;
-		introf;
-		tclCOMPLETE (wrap 2 true continue seq)]]])
-      backtrack
-
-(* quantifier rules (easy side) *)
-
-let forall_tac backtrack continue seq=
-  tclORELSE
-    (tclIFTHENELSE intro (wrap 0 true continue seq)
-       (tclORELSE
-	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
-	  backtrack))
-    (if !qflag then 
-       tclFAIL 0 (Pp.str "reversible in 1st order mode")
-     else
-       backtrack)
-
-let left_exists_tac ind backtrack id continue seq gls=
-  let n=(construct_nhyps ind gls).(0) in  
-    tclIFTHENELSE
-      (simplest_elim (constr_of_global id))
-      (tclTHENLIST [clear_global id;
-                    tclDO n intro;
-                    (wrap (n-1) false continue seq)]) 
-      backtrack 
-      gls
-	
-let ll_forall_tac prod backtrack id continue seq=
-  tclORELSE
-    (tclTHENS (cut prod)
-       [tclTHENLIST
-	  [intro;
-	   (fun gls->
-	      let id0=pf_nth_hyp_id gls 1 in
-	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls);  
-	   clear_global id;
-	   intro;
-	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
-	tclCOMPLETE (wrap 0 true continue (deepen seq))])
-    backtrack
-
-(* rules for instantiation with unification moved to instances.ml *)
-
-(* special for compatibility with old Intuition *)
-
-let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
-
-let defined_connectives=lazy
-  [[],EvalConstRef (destConst (constant "not"));
-   [],EvalConstRef (destConst (constant "iff"))]
-
-let normalize_evaluables=
-  onAllClauses
-    (function 
-	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some ((_,id),_)-> 
-	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   (([],id),Tacexpr.InHypTypeOnly))
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
deleted file mode 100644
index 3798d8d4..00000000
--- a/contrib/first-order/rules.mli
+++ /dev/null
@@ -1,54 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: rules.mli 6141 2004-09-27 14:55:34Z corbinea $ *)
-
-open Term
-open Tacmach
-open Names
-open Libnames
-
-type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
-
-type lseqtac= global_reference -> seqtac
-
-type 'a with_backtracking = tactic -> 'a
-
-val wrap : int -> bool -> seqtac
-
-val id_of_global: global_reference -> identifier
-
-val clear_global: global_reference -> tactic
-
-val axiom_tac : constr -> Sequent.t -> tactic
-
-val ll_atom_tac : constr -> lseqtac with_backtracking
-
-val and_tac : seqtac with_backtracking
-
-val or_tac : seqtac with_backtracking
-
-val arrow_tac : seqtac with_backtracking
-
-val left_and_tac : inductive -> lseqtac with_backtracking
-
-val left_or_tac : inductive -> lseqtac with_backtracking
-
-val left_false_tac : global_reference -> tactic
-
-val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
-
-val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
-
-val forall_tac : seqtac with_backtracking
-
-val left_exists_tac : inductive -> lseqtac with_backtracking
-
-val ll_forall_tac : types -> lseqtac with_backtracking 
-
-val normalize_evaluables : tactic
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
deleted file mode 100644
index 805700b0..00000000
--- a/contrib/first-order/sequent.ml
+++ /dev/null
@@ -1,303 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: sequent.ml 7925 2006-01-24 23:20:39Z herbelin $ *)
-
-open Term
-open Util
-open Formula
-open Unify
-open Tacmach
-open Names
-open Libnames
-open Pp
-
-let newcnt ()=
-  let cnt=ref (-1) in
-    fun b->if b then incr cnt;!cnt
-
-let priority = (* pure heuristics, <=0 for non reversible *)
-  function
-      Right rf->
-	begin
-	  match rf with
-	      Rarrow               -> 100
-	    | Rand                 ->  40 
-	    | Ror                  -> -15
-	    | Rfalse               -> -50
-	    | Rforall              -> 100
-	    | Rexists (_,_,_)      -> -29
-	end
-    | Left lf ->
-	match lf with
-	    Lfalse                 -> 999
-	  | Land _                 ->  90
-	  | Lor _                  ->  40
-	  | Lforall (_,_,_)        -> -30 
-	  | Lexists _              ->  60
-	  | LA(_,lap) ->
-	      match lap with
-		  LLatom           ->   0
-		| LLfalse (_,_)    -> 100
-		| LLand (_,_)      ->  80
-		| LLor (_,_)       ->  70
-		| LLforall _       -> -20
-		| LLexists (_,_)   ->  50
-		| LLarrow  (_,_,_) -> -10 
-
-let left_reversible lpat=(priority lpat)>0
-
-module OrderedFormula=
-struct
-  type t=Formula.t
-  let compare e1 e2=
-	(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
-end
-
-type h_item = global_reference * (int*constr) option
-
-module Hitem=
-struct 
-  type t = h_item
-  let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare 
-     =? (fun oc1 oc2 ->
-	   match oc1,oc2 with 
-	       Some (m1,c1),Some (m2,c2) -> 
-		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
-	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
-end
-
-module CM=Map.Make(OrderedConstr)
-
-module History=Set.Make(Hitem)
-
-let cm_add typ nam cm=
-  try 
-    let l=CM.find typ cm in CM.add typ (nam::l) cm
-  with
-      Not_found->CM.add typ [nam] cm
-	
-let cm_remove typ nam cm=
-  try
-    let l=CM.find typ cm in 
-    let l0=List.filter (fun id->id<>nam) l in
-      match l0 with 
-	  []->CM.remove typ cm
-	| _ ->CM.add typ l0 cm
-      with Not_found ->cm
-
-module HP=Heap.Functional(OrderedFormula)
-
-type t=
-    {redexes:HP.t;
-     context:(global_reference list) CM.t;
-     latoms:constr list;
-     gl:types;
-     glatom:constr option;
-     cnt:counter;
-     history:History.t;
-     depth:int}
-
-let deepen seq={seq with depth=seq.depth-1}
- 
-let record item seq={seq with history=History.add item seq.history}
-
-let lookup item seq=
-  History.mem item seq.history ||
-  match item with
-      (_,None)->false
-    | (id,Some ((m,t) as c))->
-	let p (id2,o)=
-	  match o with
-	      None -> false
-	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
-	  History.exists p seq.history
-
-let rec add_formula side nam t seq gl=
-  match build_formula side nam t gl seq.cnt with
-      Left f->
-	begin
-	  match side with
-	      Concl ->
-		{seq with 
-		   redexes=HP.add f seq.redexes;
-		   gl=f.constr;
-		   glatom=None}
-	    | _ ->
-		{seq with 
-		   redexes=HP.add f seq.redexes;
-		   context=cm_add f.constr nam seq.context}
-	end
-    | Right t->
-	match side with
-	    Concl ->
-	      {seq with gl=t;glatom=Some t}
-	  | _ ->
-	      {seq with 
-		 context=cm_add t nam seq.context;
-		 latoms=t::seq.latoms}
-	      
-let re_add_formula_list lf seq=
-  let do_one f cm=
-    if f.id == dummy_id then cm
-    else cm_add f.constr f.id cm in
-  {seq with 
-     redexes=List.fold_right HP.add lf seq.redexes;
-     context=List.fold_right do_one lf seq.context}
-
-let find_left t seq=List.hd (CM.find t seq.context)
-
-(*let rev_left seq=
-  try
-    let lpat=(HP.maximum seq.redexes).pat in
-      left_reversible lpat
-  with Heap.EmptyHeap -> false
-*)
-let no_formula seq=
-  seq.redexes=HP.empty
-
-let rec take_formula seq=
-  let hd=HP.maximum seq.redexes
-  and hp=HP.remove seq.redexes in
-    if hd.id == dummy_id then
-      let nseq={seq with redexes=hp} in
-	if seq.gl==hd.constr then 
-	  hd,nseq
-	else
-	  take_formula nseq (* discarding deprecated goal *)
-    else
-      hd,{seq with 
-	    redexes=hp;
-	    context=cm_remove hd.constr hd.id seq.context}
-	
-let empty_seq depth=
-  {redexes=HP.empty;   
-   context=CM.empty;
-   latoms=[];
-   gl=(mkMeta 1);
-   glatom=None;
-   cnt=newcnt ();
-   history=History.empty;
-   depth=depth}
-
-let create_with_ref_list l depth gl=
-  let f gr seq=
-    let c=constr_of_global gr in    
-    let typ=(pf_type_of gl c) in
-      add_formula Hyp gr typ seq gl in
-    List.fold_right f l (empty_seq depth)
-
-open Auto
-
-let create_with_auto_hints l depth gl=
-  let seqref=ref (empty_seq depth) in
-  let f p_a_t =
-    match p_a_t.code with
-	Res_pf (c,_) | Give_exact c
-      | Res_pf_THEN_trivial_fail (c,_) ->
-	  (try 
-	     let gr=global_of_constr c in 
-	     let typ=(pf_type_of gl c) in
-	       seqref:=add_formula Hint gr typ !seqref gl
-	   with Not_found->())
-      | _-> () in
-  let g _ l=List.iter f l in
-  let h dbname=
-    let hdb=
-      try
-	searchtable_map dbname
-      with Not_found-> 
-	error ("Firstorder: "^dbname^" : No such Hint database") in
-      Hint_db.iter g hdb in
-    List.iter h l;
-    !seqref
-
-let print_cmap map=
-  let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) c in
-      str "| " ++ 
-      Util.prlist Printer.pr_global l ++ 
-      str " : " ++
-      Ppconstr.pr_constr_expr xc ++ 
-      cut () ++ 
-      s in
-    msgnl (v 0 
-	     (str "-----" ++ 
-	      cut () ++
-	      CM.fold print_entry map (mt ()) ++
-	      str "-----"))
-
-	
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
deleted file mode 100644
index 47fb74c7..00000000
--- a/contrib/first-order/sequent.mli
+++ /dev/null
@@ -1,66 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: sequent.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-open Term
-open Util
-open Formula
-open Tacmach
-open Names
-open Libnames
-
-module OrderedConstr: Set.OrderedType with type t=constr
-
-module CM: Map.S with type key=constr
-
-type h_item = global_reference * (int*constr) option
-
-module History: Set.S with type elt = h_item
-
-val cm_add : constr -> global_reference -> global_reference list CM.t ->
-  global_reference list CM.t
-
-val cm_remove : constr -> global_reference -> global_reference list CM.t ->
-  global_reference list CM.t
-
-module HP: Heap.S with type elt=Formula.t
-
-type t = {redexes:HP.t;
-	  context: global_reference list CM.t;
-	  latoms:constr list;
-	  gl:types;
-	  glatom:constr option;
-	  cnt:counter;
-	  history:History.t;
-	  depth:int}
-
-val deepen: t -> t
-
-val record: h_item -> t -> t
-
-val lookup: h_item -> t -> bool
-
-val add_formula : side -> global_reference -> constr -> t -> 
-  Proof_type.goal sigma -> t
-
-val re_add_formula_list : Formula.t list -> t -> t
-
-val find_left : constr -> t -> global_reference
-
-val take_formula : t -> Formula.t * t
-
-val empty_seq : int -> t
-
-val create_with_ref_list : global_reference list ->
-  int -> Proof_type.goal sigma -> t
-
-val create_with_auto_hints : Auto.hint_db_name list -> 
-  int -> Proof_type.goal sigma -> t
-
-val print_cmap: global_reference list CM.t -> unit 
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
deleted file mode 100644
index 1dd13cbe..00000000
--- a/contrib/first-order/unify.ml
+++ /dev/null
@@ -1,143 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
-
-open Util
-open Formula 
-open Tacmach
-open Term
-open Names
-open Termops
-open Reductionops
-
-exception UFAIL of constr*constr
-
-(* 
-   RIGID-only Martelli-Montanari style unification for CLOSED terms 
-   I repeat : t1 and t2 must NOT have ANY free deBruijn                        
-   sigma is kept normal with respect to itself but is lazily applied 
-   to the equation set. Raises UFAIL with a pair of  terms 
-*)
-
-let unif t1 t2= 
-  let bige=Queue.create () 
-  and sigma=ref [] in
-  let bind i t=
-    sigma:=(i,t)::
-      (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
-  let rec head_reduce t= 
-    (* forbids non-sigma-normal meta in head position*)
-    match kind_of_term t with
-	Meta i->
-	  (try 
-	     head_reduce (List.assoc i !sigma) 
-	   with Not_found->t)
-      | _->t in 
-    Queue.add (t1,t2) bige;
-    try while true do
-      let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta t1) 
-      and nt2=head_reduce (whd_betaiotazeta t2) in
-	match (kind_of_term nt1),(kind_of_term nt2) with
-	    Meta i,Meta j-> 
-	      if i<>j then 
-		if i<j then bind j nt1
-		else bind i nt2
-	  | Meta i,_ ->
-	      let t=subst_meta !sigma nt2 in
-		if Intset.is_empty (free_rels t) && 
-		  not (occur_term (mkMeta i) t) then
-		    bind i t else raise (UFAIL(nt1,nt2))
-	  | _,Meta i -> 
-	      let t=subst_meta !sigma nt1 in
-		if Intset.is_empty (free_rels t) && 
-		  not (occur_term (mkMeta i) t) then
-		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
-	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
-	      Queue.add (pa,pb) bige;
-	      Queue.add (ca,cb) bige;
-	      let l=Array.length va in
-		if l<>(Array.length vb) then 
-		  raise (UFAIL (nt1,nt2))
-		else 
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done	  
-	  | App(ha,va),App(hb,vb)->
-	      Queue.add (ha,hb) bige;
-	      let l=Array.length va in
-		if l<>(Array.length vb) then 
-		  raise (UFAIL (nt1,nt2))
-		else 
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done
-	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
-    done;
-      assert false 
-	(* this place is unreachable but needed for the sake of typing *)
-    with Queue.Empty-> !sigma
-
-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 
-      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
-    vaux t
-	  
-type instance=
-    Real of (int*constr)*int 
-  | Phantom of constr 
-
-let mk_rel_inst t=
-  let new_rel=ref 1 in
-  let rel_env=ref [] in
-  let rec renum_rec d t=
-    match kind_of_term t with 
-	Meta n->
-	  (try 
-	     mkRel (d+(List.assoc n !rel_env))
-	   with Not_found->
-	     let m= !new_rel in
-	       incr new_rel;
-	       rel_env:=(n,m) :: !rel_env;
-	       mkRel (m+d))
-      | _ -> map_constr_with_binders succ renum_rec d t
-  in 
-  let nt=renum_rec 0 t in (!new_rel - 1,nt)
-
-let unif_atoms i dom t1 t2=
-  try 
-    let t=List.assoc i (unif t1 t2) in 
-      if isMeta t then Some (Phantom dom)
-      else Some (Real(mk_rel_inst t,value i t1))
-  with
-      UFAIL(_,_) ->None
-    | Not_found ->Some (Phantom dom)
-	   	  
-let renum_metas_from k n t= (* requires n = max (free_rels t) *)
-  let l=list_tabulate (fun i->mkMeta (k+i)) n in
-    substl l t
-
-let more_general (m1,t1) (m2,t2)=
-  let mt1=renum_metas_from 0 m1 t1
-  and mt2=renum_metas_from m1 m2 t2 in
-    try 
-      let sigma=unif mt1 mt2 in
-      let p (n,t)= n<m1 || isMeta t in
-	List.for_all p sigma
-    with UFAIL(_,_)->false
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
deleted file mode 100644
index 9fbe3dda..00000000
--- a/contrib/first-order/unify.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: unify.mli 5920 2004-07-16 20:01:26Z herbelin $ *)
-
-open Term
-
-exception UFAIL of constr*constr
-
-val unif : constr -> constr -> (int*constr) list
-
-type instance=
-    Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
-  | Phantom of constr        (* domaine de quantification *)
-
-val unif_atoms : metavariable -> constr -> constr -> constr -> instance option
-
-val more_general : (int*constr) -> (int*constr) -> bool