Added the Ground tactic.

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

16 files changed, 1250 insertions, 7 deletions

diff --git a/.depend b/.depend
index 232aa1faa8..0f288c9f3c 100644
--- a/.depend
+++ b/.depend
@@ -400,6 +400,15 @@ contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     lib/pp.cmi 
 contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
+contrib/first-order/formula.cmi: kernel/names.cmi kernel/sign.cmi \
+    kernel/term.cmi 
+contrib/first-order/rules.cmi: contrib/first-order/formula.cmi \
+    kernel/names.cmi contrib/first-order/sequent.cmi proofs/tacmach.cmi \
+    kernel/term.cmi 
+contrib/first-order/sequent.cmi: contrib/first-order/formula.cmi lib/heap.cmi \
+    kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi 
+contrib/first-order/unify.cmi: contrib/first-order/sequent.cmi \
+    kernel/term.cmi 
 contrib/funind/tacinvutils.cmi: interp/coqlib.cmi tactics/equality.cmi \
     pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi lib/pp.cmi \
     parsing/printer.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \
@@ -733,6 +742,8 @@ lib/gset.cmo: lib/gset.cmi
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
+lib/heap.cmo: lib/heap.cmi 
+lib/heap.cmx: lib/heap.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
@@ -2305,6 +2316,40 @@ translate/ppvernacnew.cmx: parsing/ast.cmx interp/constrextern.cmx \
     pretyping/rawterm.cmx interp/reserve.cmx proofs/tacexpr.cmx \
     tactics/tacinterp.cmx pretyping/termops.cmx interp/topconstr.cmx \
     lib/util.cmx toplevel/vernacexpr.cmx translate/ppvernacnew.cmi 
+user-contrib/formula.cmo: interp/coqlib.cmi kernel/declarations.cmi \
+    library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
+    kernel/names.cmi pretyping/reductionops.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+user-contrib/formula.cmx: interp/coqlib.cmx kernel/declarations.cmx \
+    library/global.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
+    kernel/names.cmx pretyping/reductionops.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
+user-contrib/rules.cmo: kernel/declarations.cmi \
+    contrib/first-order/formula.cmi kernel/names.cmi pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
+    contrib/first-order/unify.cmi lib/util.cmi 
+user-contrib/rules.cmx: kernel/declarations.cmx \
+    contrib/first-order/formula.cmx kernel/names.cmx pretyping/rawterm.cmx \
+    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
+    contrib/first-order/unify.cmx lib/util.cmx 
+user-contrib/sequent.cmo: interp/constrextern.cmi \
+    contrib/first-order/formula.cmi library/global.cmi kernel/names.cmi \
+    lib/pp.cmi parsing/ppconstr.cmi proofs/tacmach.cmi kernel/term.cmi \
+    lib/util.cmi 
+user-contrib/sequent.cmx: interp/constrextern.cmx \
+    contrib/first-order/formula.cmx library/global.cmx kernel/names.cmx \
+    lib/pp.cmx parsing/ppconstr.cmx proofs/tacmach.cmx kernel/term.cmx \
+    lib/util.cmx 
+user-contrib/unify.cmo: proofs/clenv.cmi contrib/first-order/formula.cmi \
+    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi 
+user-contrib/unify.cmx: proofs/clenv.cmx contrib/first-order/formula.cmx \
+    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx 
 contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi 
 contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi 
 contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \
@@ -2721,6 +2766,54 @@ contrib/field/field.cmx: toplevel/cerrors.cmx interp/constrintern.cmx \
     proofs/tacmach.cmx tactics/tacticals.cmx kernel/term.cmx \
     interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
     toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx 
+contrib/first-order/engine.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
+    contrib/first-order/formula.cmi interp/genarg.cmi parsing/pcoq.cmi \
+    lib/pp.cmi parsing/pptactic.cmi proofs/refiner.cmi \
+    contrib/first-order/rules.cmi contrib/first-order/sequent.cmi \
+    proofs/tacexpr.cmo tactics/tacinterp.cmi proofs/tacmach.cmi \
+    tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi 
+contrib/first-order/engine.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
+    contrib/first-order/formula.cmx interp/genarg.cmx parsing/pcoq.cmx \
+    lib/pp.cmx parsing/pptactic.cmx proofs/refiner.cmx \
+    contrib/first-order/rules.cmx contrib/first-order/sequent.cmx \
+    proofs/tacexpr.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \
+    tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx 
+contrib/first-order/formula.cmo: interp/coqlib.cmi kernel/declarations.cmi \
+    library/global.cmi tactics/hipattern.cmi pretyping/inductiveops.cmi \
+    kernel/names.cmi pretyping/reductionops.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi pretyping/termops.cmi lib/util.cmi \
+    contrib/first-order/formula.cmi 
+contrib/first-order/formula.cmx: interp/coqlib.cmx kernel/declarations.cmx \
+    library/global.cmx tactics/hipattern.cmx pretyping/inductiveops.cmx \
+    kernel/names.cmx pretyping/reductionops.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
+    contrib/first-order/formula.cmi 
+contrib/first-order/rules.cmo: kernel/declarations.cmi \
+    contrib/first-order/formula.cmi kernel/names.cmi pretyping/rawterm.cmi \
+    pretyping/reductionops.cmi contrib/first-order/sequent.cmi \
+    kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \
+    tactics/tactics.cmi kernel/term.cmi pretyping/termops.cmi \
+    contrib/first-order/unify.cmi lib/util.cmi contrib/first-order/rules.cmi 
+contrib/first-order/rules.cmx: kernel/declarations.cmx \
+    contrib/first-order/formula.cmx kernel/names.cmx pretyping/rawterm.cmx \
+    pretyping/reductionops.cmx contrib/first-order/sequent.cmx \
+    kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
+    tactics/tactics.cmx kernel/term.cmx pretyping/termops.cmx \
+    contrib/first-order/unify.cmx lib/util.cmx contrib/first-order/rules.cmi 
+contrib/first-order/sequent.cmo: contrib/first-order/formula.cmi lib/heap.cmi \
+    kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
+    contrib/first-order/sequent.cmi 
+contrib/first-order/sequent.cmx: contrib/first-order/formula.cmx lib/heap.cmx \
+    kernel/names.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
+    contrib/first-order/sequent.cmi 
+contrib/first-order/unify.cmo: proofs/clenv.cmi \
+    contrib/first-order/formula.cmi pretyping/reductionops.cmi \
+    contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
+    pretyping/termops.cmi lib/util.cmi contrib/first-order/unify.cmi 
+contrib/first-order/unify.cmx: proofs/clenv.cmx \
+    contrib/first-order/formula.cmx pretyping/reductionops.cmx \
+    contrib/first-order/sequent.cmx proofs/tacmach.cmx kernel/term.cmx \
+    pretyping/termops.cmx lib/util.cmx contrib/first-order/unify.cmi 
 contrib/fourier/fourierR.cmo: proofs/clenv.cmi tactics/contradiction.cmi \
     interp/coqlib.cmi tactics/equality.cmi contrib/fourier/fourier.cmo \
     library/libnames.cmi library/library.cmi kernel/names.cmi \
@@ -3355,6 +3448,8 @@ contrib/linear/dpc.cmo: parsing/grammar.cma
 contrib/linear/dpc.cmx: parsing/grammar.cma
 contrib/funind/tacinv.cmo: parsing/grammar.cma
 contrib/funind/tacinv.cmx: parsing/grammar.cma
+contrib/first-order/engine.cmo: parsing/grammar.cma
+contrib/first-order/engine.cmx: parsing/grammar.cma
 parsing/lexer.cmo: 
 parsing/lexer.cmx: 
 parsing/q_util.cmo: 
diff --git a/.depend.camlp4 b/.depend.camlp4
index c607a972c2..e17db259d9 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -20,6 +20,7 @@ contrib/cc/cctac.ml: parsing/grammar.cma
 contrib/linear/ccidpc.ml: parsing/grammar.cma
 contrib/linear/dpc.ml: parsing/grammar.cma
 contrib/funind/tacinv.ml: parsing/grammar.cma
+contrib/first-order/engine.ml: parsing/grammar.cma
 parsing/lexer.ml: 
 parsing/q_util.ml: 
 parsing/q_coqast.ml: 
diff --git a/Makefile b/Makefile
index 82a7e8d53d..9d5d13aa63 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,7 @@
 
 # $Id$ 
 
+
 # Makefile for Coq
 #
 # To be used with GNU Make.
@@ -46,7 +47,7 @@ LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
 	      -I contrib/extraction -I contrib/correctness \
               -I contrib/interface -I contrib/fourier \
 	      -I contrib/jprover -I contrib/cc -I contrib/linear \
-	      -I contrib/funind
+	      -I contrib/funind -I contrib/first-order
 
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
@@ -83,7 +84,8 @@ LIBREP=\
   lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
   lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
   lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
-  lib/predicate.cmo lib/rtree.cmo  # Rem: Cygwin already uses variable LIB 
+  lib/predicate.cmo lib/rtree.cmo lib/heap.cmo
+# Rem: Cygwin already uses variable LIB 
 
 KERNEL=\
   kernel/names.cmo kernel/univ.cmo \
@@ -273,6 +275,11 @@ JPROVERCMO=\
 FUNINDCMO=\
   contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo 
 
+FOCMO=\
+  contrib/first-order/formula.cmo contrib/first-order/sequent.cmo \
+  contrib/first-order/unify.cmo contrib/first-order/rules.cmo \
+  contrib/first-order/engine.cmo
+
 CCCMO=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo  
 
 LINEARCMO=\
@@ -288,11 +295,21 @@ LINEARCMO=\
   contrib/linear/dpc.cmo
 
 ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/cctac.ml4 \
-  contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 contrib/funind/tacinv.ml4
+  contrib/linear/ccidpc.ml4 contrib/linear/dpc.ml4 contrib/funind/tacinv.ml4 \
+  contrib/first-order/engine.ml4
+
+USERCMO =\
+	user-contrib/formula.cmo \
+	user-contrib/prio.cmo \
+	user-contrib/sequent.cmo \
+	user-contrib/unify.cmo \
+	user-contrib/rules.cmo \
+	user-contrib/engine.cmo
+
 
 CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \
 	$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
-	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(FUNINDCMO) $(USERCMO)
+	$(CORRECTNESSCMO) $(CCCMO) $(LINEARCMO) $(FUNINDCMO) $(FOCMO)
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
diff --git a/contrib/first-order/engine.ml4 b/contrib/first-order/engine.ml4
new file mode 100644
index 0000000000..8b85316a90
--- /dev/null
+++ b/contrib/first-order/engine.ml4
@@ -0,0 +1,105 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \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$ *)
+
+open Formula
+open Sequent
+open Rules
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Util
+
+let mytac ninst solver gl=
+  let metagen=newcnt () in
+  let rec toptac ninst seq gl=
+    match seq.gl with 
+	Atomic t->
+	  tclORELSE (axiom_tac t seq) (left_tac ninst seq []) gl
+      | Complex (pat,l)->
+	  match pat with
+	      Rand->and_tac seq (toptac ninst) metagen gl
+	    | Rforall->forall_tac seq (toptac ninst) metagen gl
+	    | Rarrow->arrow_tac seq (toptac ninst) metagen gl
+	    | _->
+		if not (is_empty_left seq) && rev_left seq then 
+		  left_tac ninst seq [] gl 
+		else 
+		  right_tac ninst seq pat l [] gl
+  and right_tac ninst seq pat atoms ctx gl=
+    let re_add s=re_add_left_list ctx s in
+      match pat with
+	  Ror->
+	    tclORELSE
+	    (or_tac (re_add seq) (toptac ninst) metagen)
+	    (left_tac ninst seq ctx) gl
+	| Rexists(i,dom)->
+	    tclORELSE
+	    (if ninst=0 then tclFAIL 0 "max depth" else 
+	       exists_tac i dom atoms (re_add seq) (toptac (ninst-1)) metagen)
+	    (left_tac ninst seq ctx) gl
+	| _-> anomaly "unreachable place"
+  and left_tac ninst seq ctx gl=
+    if is_empty_left seq then 
+      solver gl (* put solver here *)
+    else 
+      let (hd,seq1)=take_left seq in 
+      let re_add s=re_add_left_list ctx s in 
+	match hd.pat with
+	    Lfalse->left_false_tac hd.id gl
+	  | Land ind->left_and_tac ind hd.id seq1 (toptac ninst) metagen gl
+	  | Lor ind->left_or_tac ind hd.id seq1 (toptac ninst) metagen gl
+	  | Lforall (i,dom)->
+	      tclORELSE
+	      (if ninst=0 then tclFAIL 0 "max depth" else 
+		 left_forall_tac i dom hd.atoms hd.id (re_add seq)
+		   (toptac (ninst-1)) metagen)
+	      (left_tac ninst seq1 (hd::ctx)) gl
+	  | Lexists ->left_exists_tac hd.id seq1 (toptac ninst) metagen gl
+	  | LAatom a->
+	      let pat,atoms=
+		match seq1.gl with 
+		    Atomic t->assert false
+		  | Complex (pat,atoms)->pat,atoms in
+	      tclORELSE 
+	      (ll_atom_tac a hd.id (re_add seq1) (toptac ninst) metagen)
+	      (right_tac ninst seq1 pat atoms (hd::ctx)) gl
+	  | LAfalse->ll_false_tac hd.id seq1 (toptac ninst) metagen gl
+	  | LAand (ind,largs) | LAor(ind,largs) ->
+	      ll_ind_tac ind largs hd.id seq1 (toptac ninst) metagen gl
+	  | LAforall p ->	      
+	      tclORELSE
+	      (if ninst=0 then tclFAIL 0 "max depth" else 
+		 ll_forall_tac p hd.id (re_add seq1) 
+		   (toptac (ninst-1)) metagen)
+	      (left_tac ninst seq1 (hd::ctx)) gl
+	  | LAexists (ind,a,p,_) ->
+	      ll_ind_tac ind [a;p] hd.id seq1 (toptac ninst) metagen gl
+	  | LAarrow (a,b,c) ->	      
+	      tclORELSE
+	      (ll_arrow_tac a b c hd.id (re_add seq1) 
+		   (toptac ninst) metagen)
+	      (left_tac ninst seq1 (hd::ctx)) gl in
+    wrap (List.length (pf_hyps gl)) true empty_seq (toptac ninst) metagen gl
+
+let default_solver=Tacinterp.interp <:tactic<Auto with *>>
+    
+let default_depth=5
+
+TACTIC EXTEND Ground
+   [ "Ground" ] -> [ mytac default_depth default_solver]
+|  [ "Ground" integer(n)] -> [ mytac n default_solver]
+|  [ "Ground" tactic(t)] -> [ mytac default_depth (snd t)]    
+|  [ "Ground" integer(n) tactic(t)] -> [ mytac n (snd t)]
+END
+
+ 
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
new file mode 100644
index 0000000000..aee1c01d07
--- /dev/null
+++ b/contrib/first-order/formula.ml
@@ -0,0 +1,213 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Hipattern
+open Names
+open Term
+open Termops
+open Reductionops
+open Tacmach
+open Util
+open Declarations
+
+type ('a,'b)sum=Left of 'a|Right of 'b
+
+type kind_of_formula=
+   Arrow of constr*constr
+  |And of inductive*constr list
+  |Or of inductive*constr list
+  |Exists of inductive*constr*constr*constr
+  |Forall of constr*constr
+  |Atom of constr
+  |False
+
+type counter = bool -> int
+
+let newcnt ()=
+  let cnt=ref (-1) in
+    fun b->if b then incr cnt;!cnt
+
+let constant path str ()=Coqlib.gen_constant "User" ["Init";path] str
+
+let op2bool=function Some _->true |None->false
+
+let id_ex=constant "Logic" "ex"
+let id_sig=constant "Specif" "sig"
+let id_sigT=constant "Specif" "sigT"
+let id_sigS=constant "Specif" "sigS"
+let id_not=constant "Logic" "not"
+ 
+let is_ex t = 
+  t=(id_ex ()) || 
+    t=(id_sig ()) || 
+      t=(id_sigT ()) || 
+	t=(id_sigS ())
+
+let match_with_exist_term t=
+  match kind_of_term t with
+      App(t,v)->
+	if t=id_ex () && (Array.length v)=2 then
+	  let p=v.(1) in
+	    match kind_of_term p with 
+		Lambda(na,a,b)->Some(t,a,b,p)
+	      | _ ->Some(t,v.(0),mkApp(p,[|mkRel 1|]),p)
+	else None
+    | _->None
+
+let match_with_not_term t=
+  match match_with_nottype t with 
+    | None ->
+	(match kind_of_term t with
+	     App (no,b) when no=id_not ()->Some (no,b.(0))
+	   | _->None)
+    | o -> o
+
+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 nhyps mip = 
+  let constr_types = mip.mind_nf_lc in 
+  let nhyps = nb_prod_after mip.mind_nparams in	
+    Array.map nhyps constr_types
+
+let construct_nhyps ind= nhyps (snd (Global.lookup_inductive ind))
+      
+(* builds the array of arrays of constructor hyps for (ind Vargs)*)
+let ind_hyps ind largs= 
+  let (mib,mip) = Global.lookup_inductive ind in
+    if Inductiveops.mis_is_recursive (ind,mib,mip) then 
+      failwith "no_recursion" else      
+	let n=mip.mind_nparams in
+	  if n<>(List.length largs) then anomaly "params ?" else
+	    let p=nhyps mip in
+	    let lp=Array.length p in
+	    let types= mip.mind_nf_lc in   
+	    let myhyps i=
+	      let t1=Term.prod_applist types.(i) largs in
+		fst (Sign.decompose_prod_n_assum p.(i) t1) in
+	      Array.init lp myhyps
+
+let kind_of_formula cciterm =
+  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_exist_term cciterm with
+		Some (i,a,b,p)-> Exists((destInd i),a,b,p)
+	      |_-> 
+		 match match_with_nodep_ind cciterm with
+		     None -> Atom cciterm 
+		   | Some (i,l)->
+		       let ind=destInd i in
+		       let (mib,mip) = Global.lookup_inductive ind in
+			 if Inductiveops.mis_is_recursive (ind,mib,mip) then
+			   Atom cciterm 
+			 else
+			   match Array.length mip.mind_consnames with
+			       0->False
+			     | 1->And(ind,l)
+			     | _->Or(ind,l) 
+
+let build_atoms metagen=
+  let rec build_rec env polarity cciterm =
+    match kind_of_formula cciterm with
+	False->[]
+      | Arrow (a,b)->
+	  (build_rec env (not polarity) a)@
+	  (build_rec env polarity b)
+      | And(i,l) | Or(i,l)->
+	  let v = ind_hyps i l in
+	    Array.fold_right
+	      (fun l accu->
+		 List.fold_right 
+		 (fun (_,_,t) accu0->
+		    (build_rec env polarity t)@accu0) l accu) v []
+      | Forall(_,b)|Exists(_,_,b,_)->
+	  let var=mkMeta (metagen true) in
+	    build_rec (var::env) polarity b 
+      | Atom t->
+	  [polarity,(substnl env 0 cciterm)]
+  in build_rec []
+       
+type right_pattern =
+    Rand
+  | Ror 
+  | Rforall
+  | Rexists of int*constr
+  | Rarrow
+      
+type right_formula =
+    Complex of right_pattern*((bool*constr) list)
+  | Atomic of constr
+      
+type left_pattern=
+    Lfalse    
+  | Land of inductive
+  | Lor of inductive 
+  | Lforall of int*constr
+  | Lexists
+  | LAatom of constr
+  | LAfalse
+  | LAand of inductive*constr list
+  | LAor of inductive*constr list
+  | LAforall of constr
+  | LAexists of inductive*constr*constr*constr
+  | LAarrow of constr*constr*constr
+      
+type left_formula={id:identifier;
+		   pat:left_pattern;
+		   atoms:(bool*constr) list}
+    
+exception Is_atom of constr
+
+let build_left_entry nam typ metagen=
+  try 
+    let pattern=
+      match kind_of_formula typ with
+	  False        ->  Lfalse
+	| Atom a       ->  raise (Is_atom a)
+	| And(i,_)         ->  Land i
+	| Or(i,_)          ->  Lor i
+	| Exists (_,_,_,_) ->  Lexists
+	| Forall (d,_) -> let m=1+(metagen false) in Lforall(m,d)
+	| Arrow (a,b) ->
+	    (match kind_of_formula a with
+		 False->      LAfalse
+	       | Atom a->     LAatom a
+	       | And(i,l)->      LAand(i,l)
+	       | Or(i,l)->       LAor(i,l)
+	       | Arrow(a,c)-> LAarrow(a,c,b)
+	       | Exists(i,a,_,p)->LAexists(i,a,p,b)
+	       | Forall(_,_)->LAforall a) in    
+    let l=build_atoms metagen false typ in
+      Left {id=nam;pat=pattern;atoms=l}
+  with Is_atom a-> Right a
+
+let build_right_entry typ metagen=
+  try
+    let pattern=
+      match kind_of_formula typ with
+	  False        -> raise (Is_atom typ)
+	| Atom a       -> raise (Is_atom a)
+	| And(_,_)        -> Rand
+	| Or(_,_)         -> Ror
+	| Exists (_,d,_,_) -> 
+	    let m=1+(metagen false) in Rexists(m,d) 
+	| Forall (_,a) -> Rforall 
+	| Arrow (a,b) -> Rarrow in
+    let l=build_atoms metagen true typ in
+      Complex(pattern,l)
+  with Is_atom a-> Atomic a
+
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
new file mode 100644
index 0000000000..bb6dc030aa
--- /dev/null
+++ b/contrib/first-order/formula.mli
@@ -0,0 +1,69 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Names
+
+type ('a,'b) sum = Left of 'a | Right of 'b
+
+type kind_of_formula=
+   Arrow of constr*constr
+  |And of inductive*constr list
+  |Or of inductive*constr list
+  |Exists of inductive*constr*constr*constr
+  |Forall of constr*constr
+  |Atom of constr
+  |False
+
+type counter = bool -> int
+
+val newcnt : unit -> counter
+
+val construct_nhyps : inductive -> int array
+      
+val ind_hyps : inductive -> constr list -> Sign.rel_context array
+
+val kind_of_formula : constr -> kind_of_formula
+			
+type right_pattern =
+    Rand
+  | Ror 
+  | Rforall
+  | Rexists of int*constr
+  | Rarrow
+      
+type right_formula =
+    Complex of right_pattern*((bool*constr) list)
+  | Atomic of constr
+      
+type left_pattern=
+    Lfalse    
+  | Land of inductive
+  | Lor of inductive 
+  | Lforall of int*constr
+  | Lexists
+  | LAatom of constr
+  | LAfalse
+  | LAand of inductive*constr list
+  | LAor of inductive*constr list
+  | LAforall of constr
+  | LAexists of inductive*constr*constr*constr
+  | LAarrow of constr*constr*constr
+      
+type left_formula={id:identifier;
+		   pat:left_pattern;
+		   atoms:(bool*constr) list}
+
+val build_left_entry : 
+  identifier -> types -> counter -> (left_formula,types) sum
+
+val build_right_entry : types -> counter -> right_formula
+
+
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
new file mode 100644
index 0000000000..5e2e0a72d6
--- /dev/null
+++ b/contrib/first-order/rules.ml
@@ -0,0 +1,186 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Termops
+open Reductionops
+open Declarations
+open Formula
+open Sequent
+open Unify
+
+type hptac= Sequent.t -> (Sequent.t -> tactic) -> counter -> tactic
+
+type lhptac= identifier -> hptac
+  
+let wrap n b seq tacrec metagen gls=
+  let nc=pf_hyps gls in
+  let rec aux i nc=
+    if i<=0 then seq else 
+      match nc with
+	  []->anomaly "Not the expected number of hyps"
+	| (id,_,typ)::q-> (add_left (id,typ) (aux (i-1) q) metagen) in
+  let seq1=
+    if b then
+      (change_right (pf_concl gls) (aux n nc) metagen)
+    else
+      (aux n nc) in
+    tacrec seq1 gls
+      
+let axiom_tac t seq=
+  try exact_no_check (mkVar (find_left t seq)) 
+  with Not_found->tclFAIL 0 "No axiom link" 
+
+let and_tac seq tacrec metagen=
+  tclTHEN simplest_split (wrap 0 true seq tacrec metagen)
+
+let left_and_tac ind id seq tacrec metagen=
+  let n=(construct_nhyps ind).(0) in  
+    tclTHENLIST 
+      [simplest_elim (mkVar id);
+       clear [id]; 
+       tclDO n intro;
+       wrap n false seq tacrec metagen]
+
+let or_tac seq tacrec metagen=
+  any_constructor (Some (tclSOLVE [wrap 0 true seq tacrec metagen]))
+
+let left_or_tac ind id seq tacrec metagen=
+  let v=construct_nhyps ind in  
+  let f n=
+    tclTHENLIST
+      [clear [id];
+       tclDO n intro;
+       wrap n false seq tacrec metagen] in
+    tclTHENSV
+      (simplest_elim (mkVar id))
+      (Array.map f v)
+
+let forall_tac seq tacrec metagen=
+  tclTHEN intro (wrap 0 true seq tacrec metagen)
+
+let left_forall_tac i dom atoms id seq tacrec metagen=
+  let insts=find_instances i atoms seq in
+    if insts=[] then 
+      tclTHENS (cut dom) 
+	[tclTHENLIST
+	   [intro;
+	    (fun gls->generalize 
+	       [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+	    intro;
+	    tclSOLVE [wrap 1 false seq tacrec metagen]]
+	;tclIDTAC]
+    else
+      let tac t=
+	tclTHENLIST 
+	  [generalize [mkApp(mkVar id,[|t|])];
+	   intro; 
+	   tclSOLVE [wrap 1 false seq tacrec metagen]] in
+	tclFIRST (List.map tac insts)
+	  
+let arrow_tac seq tacrec metagen=
+  tclTHEN intro (wrap 1 true seq tacrec metagen)
+    
+let exists_tac i dom atoms seq tacrec metagen=
+  let insts=find_instances i atoms seq in
+    if insts=[] then 
+      tclTHENS (cut dom) 
+	[tclTHENLIST
+	   [intro;
+	    (fun gls->
+	       split (Rawterm.ImplicitBindings 
+			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
+	       tclSOLVE [wrap 0 false seq tacrec metagen]]
+	    ;tclIDTAC]
+	 else
+	   let tac t=
+	     tclTHEN (split (Rawterm.ImplicitBindings [t]))
+	       (tclSOLVE [wrap 0 true seq tacrec metagen]) in
+	     tclFIRST (List.map tac insts)
+	       
+let left_exists_tac id seq tacrec metagen=
+  tclTHENLIST
+    [simplest_elim (mkVar id);
+     clear [id];
+     tclDO 2 intro;
+     (wrap 1 false seq tacrec metagen)]
+
+let ll_arrow_tac a b c id seq tacrec metagen=
+  let cc=mkProd(Anonymous,a,(lift 1 b)) in
+  let d=mkLambda (Anonymous,b,
+		  mkApp ((mkVar id),
+			 [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+    tclTHENS (cut c)
+      [tclTHENLIST
+	 [intro;
+	  clear [id];
+	  wrap 1 false seq tacrec metagen];
+       tclTHENS (cut cc) 
+         [exact_no_check (mkVar id); 
+	  tclTHENLIST 
+	    [generalize [d];
+	     intro;
+	     clear [id];
+	     tclSOLVE [wrap 1 true seq tacrec metagen]]]]
+
+let ll_atom_tac a id seq tacrec metagen=
+  try 
+    tclTHENLIST
+      [generalize [mkApp(mkVar id,[|mkVar (find_left a seq)|])];
+       clear [id];
+       intro;
+       wrap 1 false seq tacrec metagen] 
+  with Not_found->tclFAIL 0 "No link" 
+
+let ll_false_tac id seq tacrec metagen=
+  tclTHEN (clear [id]) (wrap 0 false seq tacrec metagen)
+
+let left_false_tac id=
+  simplest_elim (mkVar id)
+
+(*We use this function for and, or, exists*)
+
+let ll_ind_tac ind largs id seq tacrec metagen gl= 
+  (try
+     let rcs=ind_hyps ind largs 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 (mkVar id)),[|capply|]) in
+	 Sign.it_mkLambda_or_LetIn head rc in
+       let lp=Array.length rcs in
+       let newhyps=List.map myterm (interval 0 (lp-1)) in
+	 tclTHENLIST 
+	   [generalize newhyps;
+	    clear [id];
+	    tclDO lp intro;
+	    wrap lp false seq tacrec metagen]
+   with Invalid_argument _ ->tclFAIL 0 "") gl
+
+let ll_forall_tac prod id seq tacrec metagen=
+  tclTHENS (cut prod)
+    [tclTHENLIST
+       [(fun gls->generalize 
+	   [mkApp(mkVar id,[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
+	clear [id];
+	intro;
+	tclSOLVE [wrap 1 false seq tacrec metagen]];
+       tclSOLVE [wrap 0 true seq tacrec metagen]]
+
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
new file mode 100644
index 0000000000..98dc01bbed
--- /dev/null
+++ b/contrib/first-order/rules.mli
@@ -0,0 +1,51 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Tacmach
+open Names
+
+type hptac= Sequent.t -> (Sequent.t -> tactic) -> Formula.counter -> tactic
+
+type lhptac= identifier -> hptac
+
+val wrap : int -> bool -> hptac
+
+val axiom_tac : constr -> Sequent.t -> tactic
+
+val and_tac : hptac
+
+val left_and_tac : inductive -> lhptac
+
+val or_tac : hptac
+
+val left_or_tac : inductive -> lhptac
+
+val forall_tac : hptac
+
+val left_forall_tac : int -> types -> (bool * constr) list -> lhptac
+
+val arrow_tac : hptac
+
+val exists_tac : int -> types -> (bool * constr) list -> hptac
+	       
+val left_exists_tac : lhptac
+
+val ll_arrow_tac : constr -> constr -> constr -> lhptac
+
+val ll_atom_tac : constr -> lhptac
+
+val ll_false_tac : lhptac
+
+val left_false_tac : identifier -> tactic
+
+val ll_ind_tac : inductive -> constr list -> lhptac
+
+val ll_forall_tac : types -> lhptac
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
new file mode 100644
index 0000000000..84e3f18ed4
--- /dev/null
+++ b/contrib/first-order/sequent.ml
@@ -0,0 +1,97 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util
+open Formula
+open Tacmach
+open Names
+
+let priority=function (* pure heuristics, <=0 for non reversible *)
+      Lfalse             ->1000
+    | Land _             ->  90
+    | Lor _              ->  40
+    | Lforall (_,_)      -> -20
+    | Lexists            ->  60
+    | LAatom _           ->   0
+    | LAfalse            -> 100
+    | LAand (_,_)      ->  80
+    | LAor (_,_)       ->  70
+    | LAforall _         -> -30
+    | LAexists (_,_,_,_) ->  50
+    | LAarrow  (_,_,_)   ->   -10 
+
+
+let right_atomic=function
+    Atomic _->true
+  | Complex (_,_) ->false
+      
+let right_reversible=
+  function
+      Rarrow | Rand | Rforall->true
+    | _ ->false
+	
+let left_reversible lpat=(priority lpat)>0
+
+module OrderedFormula=
+struct
+  type t=left_formula
+  let compare e1 e2=(priority e1.pat) - (priority e2.pat)
+end
+
+module OrderedConstr=
+struct
+  type t=constr
+  let compare=Pervasives.compare
+end
+
+module CM=Map.Make(OrderedConstr)
+
+module HP=Heap.Functional(OrderedFormula)
+
+type t=
+    {hyps:HP.t;hatoms:identifier CM.t;gl:right_formula}
+
+let add_left (nam,t) seq metagen=
+  match build_left_entry nam t metagen with
+      Left f->{seq with hyps=HP.add f seq.hyps}
+    | Right t->{seq with hatoms=CM.add t nam seq.hatoms}
+
+let re_add_left_list lf seq=
+  {seq with hyps=List.fold_right HP.add lf seq.hyps} 
+
+let change_right t seq metagen=
+  {seq with gl=build_right_entry t metagen}
+
+let find_left t seq=CM.find t seq.hatoms
+
+let atomic_right seq= right_atomic seq.gl 
+
+let rev_left seq=
+  try
+    let lpat=(HP.maximum seq.hyps).pat in
+      left_reversible lpat
+  with Heap.EmptyHeap -> false
+
+let is_empty_left seq=
+  seq.hyps=HP.empty
+
+let take_left seq=
+  let hd=HP.maximum seq.hyps
+  and hp=HP.remove seq.hyps in
+    hd,{seq with hyps=hp}
+
+let take_right seq=seq.gl
+
+let empty_seq=
+  {hyps=HP.empty;
+   hatoms=CM.empty;
+   gl=Atomic (mkMeta 1)}
+
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli
new file mode 100644
index 0000000000..8b72b3f210
--- /dev/null
+++ b/contrib/first-order/sequent.mli
@@ -0,0 +1,44 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util
+open Formula
+open Tacmach
+open Names
+
+val right_reversible : right_pattern -> bool
+	
+val left_reversible : left_pattern -> bool
+
+module CM: Map.S with type key=constr
+
+module HP: Heap.S with type elt=left_formula
+
+type t = {hyps:HP.t;hatoms: identifier CM.t;gl:right_formula}
+
+val add_left : identifier * constr -> t -> counter -> t
+
+val re_add_left_list : left_formula list -> t -> t
+
+val change_right : constr -> t -> counter -> t
+
+val find_left : constr -> t -> identifier
+
+val rev_left : t -> bool
+
+val is_empty_left : t -> bool
+
+val take_left : t -> left_formula * t
+
+val take_right : t -> right_formula
+
+val empty_seq : t
+
diff --git a/contrib/first-order/unify.ml b/contrib/first-order/unify.ml
new file mode 100644
index 0000000000..9d6bb39d31
--- /dev/null
+++ b/contrib/first-order/unify.ml
@@ -0,0 +1,131 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Util
+open Formula 
+open Sequent
+open Tacmach
+open Term
+open Termops
+open Reductionops
+
+exception UFAIL of constr*constr
+
+let unif t1 t2= (* Martelli-Montanari style *)
+  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
+      
+(* collect tries finds ground instantiations for Meta i*)
+let is_ground t=(Clenv.collect_metas t)=[]
+
+let collect i l=
+  try
+    let t=List.assoc i l in 
+      if is_ground t then Some t else None
+  with Not_found->None
+
+let unif_atoms_for_meta i (b1,t1) (b2,t2)=
+  if b1=b2 then None else
+    try 
+      collect i (unif t1 t2) 
+    with UFAIL(_,_) ->None
+    
+module OrderedConstr=
+struct
+  type t=constr
+  let compare=Pervasives.compare
+end
+
+module CS=Set.Make(OrderedConstr)
+
+let match_atom_list i atom l=
+  let f atom2 accu=
+    match unif_atoms_for_meta i atom atom2 with
+	None-> accu
+      | Some t-> CS.add t accu in
+    List.fold_right f l CS.empty
+
+let match_lists i l1 l2=
+  let f atom accu=
+    CS.union (match_atom_list i atom l2) accu in
+    List.fold_right f l1 CS.empty
+      
+let find_instances i l seq=
+  let match_hyp f accu=
+    CS.union (match_lists i l f.atoms) accu in
+  let match_atom t nam accu=
+    CS.union (match_atom_list i (false,t) l) accu in
+  let s1=
+    match seq.gl with 
+	Atomic t->(match_atom_list i (true,t) l)
+      | Complex(_,l1)->(match_lists i l l1) in
+  let s2=CM.fold match_atom seq.hatoms s1 in
+  let s3=HP.fold match_hyp seq.hyps s2 in
+    CS.fold (fun x l->x::l) s3 []
+
diff --git a/contrib/first-order/unify.mli b/contrib/first-order/unify.mli
new file mode 100644
index 0000000000..04d7951014
--- /dev/null
+++ b/contrib/first-order/unify.mli
@@ -0,0 +1,13 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Term
+
+val find_instances : int -> (bool * constr) list -> Sequent.t -> constr list
diff --git a/lib/heap.ml b/lib/heap.ml
new file mode 100644
index 0000000000..8b8f1ef1b1
--- /dev/null
+++ b/lib/heap.ml
@@ -0,0 +1,153 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(*s Heaps *)
+
+module type Ordered = sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S =sig
+  
+  (* Type of functional heaps *)
+  type t
+
+  (* Type of elements *)
+  type elt
+    
+  (* The empty heap *)
+  val empty : t
+    
+  (* [add x h] returns a new heap containing the elements of [h], plus [x];
+     complexity $O(log(n))$ *)
+  val add : elt -> t -> t
+    
+  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
+     when [h] is empty; complexity $O(1)$ *)
+  val maximum : t -> elt
+    
+  (* [remove h] returns a new heap containing the elements of [h], except
+     the maximum of [h]; raises [EmptyHeap] when [h] is empty; 
+     complexity $O(log(n))$ *) 
+  val remove : t -> t
+    
+  (* usual iterators and combinators; elements are presented in
+     arbitrary order *)
+  val iter : (elt -> unit) -> t -> unit
+    
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    
+end
+
+exception EmptyHeap
+
+(*s Functional implementation *)
+
+module Functional(X : Ordered) = struct
+
+  (* Heaps are encoded as complete binary trees, i.e., binary trees
+     which are full expect, may be, on the bottom level where it is filled 
+     from the left. 
+     These trees also enjoy the heap property, namely the value of any node 
+     is greater or equal than those of its left and right subtrees.
+
+     There are 4 kinds of complete binary trees, denoted by 4 constructors:
+     [FFF] for a full binary tree (and thus 2 full subtrees);
+     [PPF] for a partial tree with a partial left subtree and a full
+     right subtree;
+     [PFF] for a partial tree with a full left subtree and a full right subtree
+     (but of different heights);
+     and [PFP] for a partial tree with a full left subtree and a partial
+     right subtree. *)
+
+  type t = 
+    | Empty
+    | FFF of t * X.t * t (* full    (full,    full) *)
+    | PPF of t * X.t * t (* partial (partial, full) *)
+    | PFF of t * X.t * t (* partial (full,    full) *)
+    | PFP of t * X.t * t (* partial (full,    partial) *)
+
+  type elt = X.t
+
+  let empty = Empty
+ 
+  (* smart constructors for insertion *)
+  let p_f l x r = match l with
+    | Empty | FFF _ -> PFF (l, x, r)
+    | _ -> PPF (l, x, r)
+
+  let pf_ l x = function
+    | Empty | FFF _ as r -> FFF (l, x, r)
+    | r -> PFP (l, x, r)
+
+  let rec add x = function
+    | Empty -> 
+	FFF (Empty, x, Empty)
+    (* insertion to the left *)
+    | FFF (l, y, r) | PPF (l, y, r) ->
+	if X.compare x y > 0 then p_f (add y l) x r else p_f (add x l) y r
+    (* insertion to the right *)
+    | PFF (l, y, r) | PFP (l, y, r) ->
+	if X.compare x y > 0 then pf_ l x (add y r) else pf_ l y (add x r)
+
+  let maximum = function
+    | Empty -> raise EmptyHeap
+    | FFF (_, x, _) | PPF (_, x, _) | PFF (_, x, _) | PFP (_, x, _) -> x
+
+  (* smart constructors for removal; note that they are different
+     from the ones for insertion! *)
+  let p_f l x r = match l with
+    | Empty | FFF _ -> FFF (l, x, r)
+    | _ -> PPF (l, x, r)
+
+  let pf_ l x = function
+    | Empty | FFF _ as r -> PFF (l, x, r)
+    | r -> PFP (l, x, r)
+
+  let rec remove = function
+    | Empty -> 
+	raise EmptyHeap
+    | FFF (Empty, _, Empty) -> 
+	Empty
+    | PFF (l, _, Empty) ->
+	l
+    (* remove on the left *)
+    | PPF (l, x, r) | PFF (l, x, r) ->
+        let xl = maximum l in
+	let xr = maximum r in
+	let l' = remove l in
+	if X.compare xl xr >= 0 then 
+	  p_f l' xl r 
+	else 
+	  p_f l' xr (add xl (remove r))
+    (* remove on the right *)
+    | FFF (l, x, r) | PFP (l, x, r) ->
+        let xl = maximum l in
+	let xr = maximum r in
+	let r' = remove r in
+	if X.compare xl xr > 0 then 
+	  pf_ (add xr (remove l)) xl r'
+	else 
+	  pf_ l xr r'
+
+  let rec iter f = function
+    | Empty -> 
+	()
+    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
+	iter f l; f x; iter f r
+
+  let rec fold f h x0 = match h with
+    | Empty -> 
+	x0
+    | FFF (l, x, r) | PPF (l, x, r) | PFF (l, x, r) | PFP (l, x, r) -> 
+	fold f l (fold f r (f x x0))
+
+end
diff --git a/lib/heap.mli b/lib/heap.mli
new file mode 100644
index 0000000000..89e73af3f6
--- /dev/null
+++ b/lib/heap.mli
@@ -0,0 +1,54 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+(* Heaps *)
+
+module type Ordered = sig
+  type t
+  val compare : t -> t -> int
+end
+
+module type S =sig
+  
+  (* Type of functional heaps *)
+  type t
+
+  (* Type of elements *)
+  type elt
+    
+  (* The empty heap *)
+  val empty : t
+    
+  (* [add x h] returns a new heap containing the elements of [h], plus [x];
+     complexity $O(log(n))$ *)
+  val add : elt -> t -> t
+    
+  (* [maximum h] returns the maximum element of [h]; raises [EmptyHeap]
+     when [h] is empty; complexity $O(1)$ *)
+  val maximum : t -> elt
+    
+  (* [remove h] returns a new heap containing the elements of [h], except
+     the maximum of [h]; raises [EmptyHeap] when [h] is empty; 
+     complexity $O(log(n))$ *) 
+  val remove : t -> t
+    
+  (* usual iterators and combinators; elements are presented in
+     arbitrary order *)
+  val iter : (elt -> unit) -> t -> unit
+    
+  val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
+    
+end
+
+exception EmptyHeap
+
+(*S Functional implementation. *)
+
+module Functional(X: Ordered) : S with type elt=X.t
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index c11fd1699b..ff735c9cd5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -176,10 +176,19 @@ let match_with_nottype t =
 
 let is_nottype t = op2bool (match_with_nottype t)
 		     
-let is_imp_term c = 
+let match_with_forall_term c=
   match kind_of_term c with
-    | Prod (_,_,b) -> not (dependent (mkRel 1) b)
-    | _              -> false
+    | Prod (nam,a,b) -> Some (nam,a,b)
+    | _            -> None
+
+let is_forall_term c = op2bool (match_with_forall_term c) 
+
+let match_with_imp_term c=
+  match kind_of_term c with
+    | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b)
+    | _              -> None
+
+let is_imp_term c = op2bool (match_with_imp_term c) 
 
 let rec has_nodep_prod_after n c =
   match kind_of_term c with
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 053175269c..8beaaf65e9 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -74,6 +74,11 @@ val is_equation            : testing_function
 val match_with_nottype     : (constr * constr) matching_function
 val is_nottype             : testing_function 
 
+val match_with_forall_term    : (name * constr * constr) matching_function
+val is_forall_term            : testing_function 
+
+val match_with_imp_term    : (constr * constr) matching_function
+val is_imp_term            : testing_function 
 
 (* I added these functions to test whether a type contains dependent
   products or not, and if an inductive has constructors with dependent types