module Clenv (debut)

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

11 files changed, 1277 insertions, 121 deletions

diff --git a/.depend b/.depend
index 1c6ea061c3..b65a8a206a 100644
--- a/.depend
+++ b/.depend
@@ -51,10 +51,12 @@ parsing/pcoq.cmi: parsing/coqast.cmi
 parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
+proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
+    kernel/term.cmi lib/util.cmi 
 proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi 
-proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi proofs/proof_trees.cmi \
-    kernel/sign.cmi kernel/term.cmi 
+proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \
     proofs/refiner.cmi kernel/sign.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -64,6 +66,8 @@ proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi
 proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
     kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
     proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi 
+proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/names.cmi kernel/reduction.cmi kernel/term.cmi 
 proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -242,6 +246,14 @@ parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
+proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/clenv.cmi 
+proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
+    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/clenv.cmi 
 proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
     proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
     kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \
@@ -274,8 +286,18 @@ proofs/refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
     lib/util.cmx proofs/refiner.cmi 
-proofs/tacmach.cmo: proofs/tacmach.cmi 
-proofs/tacmach.cmx: proofs/tacmach.cmi 
+proofs/tacmach.cmo: parsing/ast.cmi kernel/environ.cmi \
+    proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \
+    kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \
+    kernel/sign.cmi lib/stamps.cmi proofs/tacred.cmi kernel/term.cmi \
+    proofs/typing_ev.cmi lib/util.cmi proofs/tacmach.cmi 
+proofs/tacmach.cmx: parsing/ast.cmx kernel/environ.cmx \
+    proofs/evar_refiner.cmx kernel/evd.cmx kernel/generic.cmx \
+    kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
+    kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx kernel/term.cmx \
+    proofs/typing_ev.cmx lib/util.cmx proofs/tacmach.cmi 
 proofs/tacred.cmo: proofs/tacred.cmi 
 proofs/tacred.cmx: proofs/tacred.cmi 
 proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
diff --git a/Makefile b/Makefile
index 465268ad0f..aaa9cd1141 100644
--- a/Makefile
+++ b/Makefile
@@ -52,7 +52,7 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
 
 PROOFS=proofs/typing_ev.cmo proofs/proof_trees.cmo proofs/logic.cmo \
-       proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo
+       proofs/refiner.cmo proofs/evar_refiner.cmo proofs/clenv.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f99a026104..c072a368b4 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -70,3 +70,5 @@ let error_ill_formed_rec_body k env str lna i vdefs =
 
 let error_ill_typed_rec_body k env i lna vdefj vargs =
   raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
+
+
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 7a1f232f17..961a1b2511 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -71,3 +71,4 @@ val error_ill_formed_rec_body :
 val error_ill_typed_rec_body  :
   path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> 'b
+
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
new file mode 100644
index 0000000000..638dea16d7
--- /dev/null
+++ b/proofs/clenv.ml
@@ -0,0 +1,1062 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Instantiate
+open Evd
+open Proof_trees
+open Logic
+open Reduction
+open Tacmach
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Intset.t }
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Intmap.t;
+  env : clbinding Intmap.t;
+  hook : 'a }
+
+type wc = walking_constraints
+
+let new_evar_in_sign env =
+  let hyps = get_globals (Environ.context env) in
+  let ev = new_evar () in
+  DOPN(Evar ev,
+       Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
+
+let rec whd_deltat wc = function
+  | DOPN(Evar ev,_) as k ->
+      if is_defined (w_Underlying wc) ev then
+        whd_deltat wc (w_const_value wc k)
+      else 
+	collapse_appl k
+  | t -> 
+      collapse_appl t
+
+let applyHead n c wc = 
+  let rec apprec n c cty wc =
+    if n = 0 then 
+      (wc,c)
+    else 
+      match w_whd_betadeltaiota wc cty with
+        | DOP2(Prod,c1,c2) ->
+            let c1ty = w_type_of wc c1 in
+	    let evar = new_evar_in_sign (w_env wc) in
+            let (evar_sp, _) = destConst evar in
+	    (compose 
+	       (apprec (n-1) (applist(c,[evar])) (sAPP c2 evar))
+	       (w_Declare evar_sp (DOP2(Cast,c1,c1ty))))
+	    wc
+	| _ -> error "Apply_Head_Then"
+  in 
+  apprec n c (w_type_of wc c) wc
+
+let mimick_evar hdc nargs sp wc =
+  (w_Focusing_THEN sp
+     (applyHead nargs hdc)
+     (fun c wc -> w_Define sp c wc)) wc
+
+
+(* Unification à l'ordre 0 de m et n: [unify_0 mc wc m n] renvoie deux listes:
+
+   metasubst:(int*constr)list    récolte les instances des (Meta k)
+   evarsubst:(constr*constr)list récolte les instances des (Const "?k")
+
+   Attention : pas d'unification entre les différences instances d'une
+   même meta ou evar, il peut rester des doublons *)
+
+let unify_0 mc wc m n =
+  let rec unirec_rec ((metasubst,evarsubst) as substn) m n =
+    let cM = whd_deltat wc m
+    and cN = whd_deltat wc n in 
+    try 
+      match (cM,cN) with
+	| DOP2(Cast,c,_),t2 -> unirec_rec substn c t2
+	| t1,DOP2(Cast,c,_) -> unirec_rec substn t1 c
+	| DOP0(Meta k),_    -> (k,cN)::metasubst,evarsubst
+	| cM,DOP0(Meta(k))    -> (k,cM)::metasubst,evarsubst
+	| DOP2(Lambda,t1,DLAM(_,c1)),DOP2(Lambda,t2,DLAM(_,c2)) ->
+	    unirec_rec (unirec_rec substn t1 t2) c1 c2
+	| DOP2(Prod,t1,DLAM(_,c1)),DOP2(Prod,t2,DLAM(_,c2)) ->
+	    unirec_rec (unirec_rec substn t1 t2) c1 c2
+
+	| DOPN(AppL,cl1),DOPN(AppL,cl2) ->
+	    let len1 = Array.length cl1
+	    and len2 = Array.length cl2 in
+	    if len1 = len2 then
+              array_fold_left2 unirec_rec substn cl1 cl2
+	    else if len1 < len2 then
+              let extras,restcl2 = array_chop ((len2-len1)+1) cl2 in 
+	      array_fold_left2 unirec_rec 
+		(unirec_rec substn (array_hd cl1) (DOPN(AppL,extras)))
+                (array_tl cl1) restcl2
+	    else 
+	      let extras,restcl1 = array_chop ((len1-len2)+1) cl1 in 
+	      array_fold_left2 unirec_rec 
+		(unirec_rec substn (DOPN(AppL,extras)) (array_hd cl2))
+                restcl1 (array_tl cl2)
+		
+	| DOPN(MutCase _,_),DOPN(MutCase _,_) ->
+	    let (_,p1,c1,cl1) = destCase cM 
+	    and (_,p2,c2,cl2) = destCase cN in
+	    if Array.length cl1 = Array.length cl2 then
+              array_fold_left2 unirec_rec 
+		(unirec_rec (unirec_rec substn p1 p2) c1 c2) cl1 cl2
+	    else 
+	      error_cannot_unify CCI (m,n)
+		
+	| DOPN(MutConstruct _,_),DOPN(MutConstruct _,_) ->
+	    if w_conv_x wc cM cN then substn else error_cannot_unify CCI (m,n)
+	      
+	| DOPN(MutInd _,_),DOPN(MutInd _,_) ->
+	    if w_conv_x wc cM cN then substn else error_cannot_unify CCI (m,n)
+	      
+	| (DOPN(Evar _,_)),(DOPN((Const _ | Evar _),_)) ->
+	    metasubst,((cM,cN)::evarsubst)
+	| (DOPN((Const _ | Evar _),_)),(DOPN(Evar _,_)) ->
+	    metasubst,((cN,cM)::evarsubst)
+	| (DOPN(Const _,_)),(DOPN(Const _,_)) ->
+	    if w_conv_x wc cM cN then 
+	      substn
+	    else 
+	      error_cannot_unify CCI (m,n)
+		
+	| (DOPN(Evar _,_)),_ ->
+	    metasubst,((cM,cN)::evarsubst)
+	| (DOPN(Const _,_)),_ ->
+	    if w_conv_x wc cM cN then 
+	      substn
+	    else 
+	      error_cannot_unify CCI (m,n)
+		
+	| _,(DOPN(Evar _,_)) ->
+	    metasubst,((cN,cM)::evarsubst)
+	| _,(DOPN(Const _,_)) ->
+	    if (not (occur_meta cM)) & w_conv_x wc cM cN then 
+	      substn
+	    else 
+	      error_cannot_unify CCI (m,n)
+		
+	| _ -> error_cannot_unify CCI (m,n)
+	      
+    with UserError _ as ex ->
+      if (not(occur_meta cM)) & w_conv_x wc cM cN then 
+	substn
+      else 
+	raise ex
+
+    in
+    if (not((occur_meta m))) & w_conv_x wc m n then 
+      (mc,[])
+    else 
+      unirec_rec (mc,[]) m n
+
+	
+let whd_castappdeltat_stack sigma = 
+  let rec whrec x l =
+    match x with
+      | DOPN(Evar ev,_) as c ->
+	  if is_defined sigma ev then
+	    whrec (existential_value sigma c) l
+	  else
+	    x,l
+      | DOP2(Cast,c,_) -> whrec c l
+      | DOPN(AppL,cl) -> whrec (array_hd cl) (array_app_tl cl l)
+      | x -> x,l
+  in 
+  whrec
+
+let whd_castappdeltat sigma c = applist(whd_castappdeltat_stack sigma c [])
+
+let w_whd wc c = whd_castappdeltat (w_Underlying wc) c
+
+(* Unification
+ *
+ * Procedure:
+ * (1) The function [unify mc wc M N] produces two lists:
+ *     (a) a list of bindings Meta->RHS
+ *     (b) a list of bindings EVAR->RHS
+ *
+ * The Meta->RHS bindings cannot themselves contain
+ * meta-vars, so they get applied eagerly to the other
+ * bindings.  This may or may not close off all RHSs of
+ * the EVARs.  For each EVAR whose RHS is closed off,
+ * we can just apply it, and go on.  For each which
+ * is not closed off, we need to do a mimick step -
+ * in general, we have something like:
+ *
+ *      ?X == (c e1 e2 ... ei[Meta(k)] ... en)
+ *
+ * so we need to do a mimick step, converting ?X
+ * into
+ *
+ *      ?X -> (c ?z1 ... ?zn)
+ *
+ * of the proper types.  Then, we can decompose the
+ * equation into
+ *
+ *      ?z1 --> e1
+ *          ...
+ *      ?zi --> ei[Meta(k)]
+ *          ...
+ *      ?zn --> en
+ *
+ * and keep on going.  Whenever we find that a R.H.S.
+ * is closed, we can, as before, apply the constraint
+ * directly.  Whenever we find an equation of the form:
+ *
+ *      ?z -> Meta(n)
+ *
+ * we can reverse the equation, put it into our metavar
+ * substitution, and keep going.
+ *
+ * The most efficient mimick possible is, for each
+ * Meta-var remaining in the term, to declare a
+ * new EVAR of the same type.  This is supposedly
+ * determinable from the clausale form context -
+ * we look up the metavar, take its type there,
+ * and apply the metavar substitution to it, to
+ * close it off.  But this might not always work,
+ * since other metavars might also need to be resolved. *)
+
+let rec w_Unify m n mc wc =
+  let (mc',ec') = unify_0 mc wc m n in 
+  w_resrec mc' ec' wc
+
+and w_resrec metas evars wc =
+  match evars with
+    | [] -> (wc,metas)
+	  
+    | (lhs,(DOP0(Meta k) as rhs))::t -> w_resrec ((k,lhs)::metas) t wc
+	  
+    | (DOPN(Const evsp,_) as evar,rhs)::t ->
+	if w_defined_const wc evar then
+          let (wc',metas') = w_Unify rhs evar metas wc in 
+	  w_resrec metas' t wc'
+	else
+          (try 
+	     w_resrec metas t (w_Define evsp rhs wc)
+           with UserError _ ->
+             (match rhs with
+             	| DOPN(AppL,cl) ->
+		    (match cl.(0) with
+		       | DOPN(Const sp,_) ->
+			   let wc' = mimick_evar cl.(0) 
+				       ((Array.length cl) - 1) evsp wc in
+			   w_resrec metas evars wc'
+		       | _ -> error "w_Unify")
+		| _ -> error "w_Unify"))
+    | _ -> anomaly "w_resrec"
+
+
+(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
+   particulier ne semblent pas vérifier que des instances différentes
+   d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
+   provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
+
+let unifyTerms m n = walking (fun wc -> fst (w_Unify m n [] wc))
+
+let unify m gls =
+  let n = pf_concl gls in unifyTerms m n gls
+
+let pr_clenv clenv =
+  let pr_name mv =
+    try 
+      let id = Intmap.find clenv.namenv mv in
+      [< 'sTR"[" ; print_id id ; 'sTR"]" >]
+    with Not_found -> 
+      [< >]
+  in
+  let pr_meta_binding = function
+    | (mv,CLTYP b) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " : " ; pTERM b.rebus ; 'fNL >]
+    | (mv,CLVAL(b,_)) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " := " ; pTERM b.rebus ; 'fNL >]
+  in
+  [< 'sTR"TEMPL: " ; pTERM clenv.templval.rebus ;
+     'sTR" : " ; pTERM clenv.templtyp.rebus ; 'fNL ;
+     (prlist pr_meta_binding (Intavm.toList clenv.env)) >]
+
+(* collects all metavar occurences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c = 
+  let rec collrec c acc =
+    match c with
+      | DOP0(Meta mv)    -> mv::acc
+      | DOP1(oper,c)     -> collrec c acc
+      | DOP2(oper,c1,c2) -> collrec c1 (collrec c2 acc)
+      | DOPN(oper,cl)    -> vect_it collrec cl acc
+      | DLAM(_,c)        -> collrec c acc
+      | DLAMV(_,v)       -> vect_it collrec v acc
+      | _                -> acc
+  in 
+  collrec c []
+
+let metavars_of c =  
+  let rec collrec c acc =
+    match c with
+      | DOP0(Meta mv)    -> Intavs.add acc mv
+      | DOP1(oper,c)     -> collrec c acc
+      | DOP2(oper,c1,c2) -> collrec c1 (collrec c2 acc)
+      | DOPN(oper,cl)    -> vect_it collrec cl acc
+      | DLAM(_,c)        -> collrec c acc
+      | DLAMV(_,v)       -> vect_it collrec v acc
+      | _                -> acc
+  in 
+  collrec c (Intavs.mt)
+
+let mk_freelisted c =
+  { rebus = c; freemetas = metavars_of c }
+
+(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
+ * mv0, or if one of the free vars on mv1's freelist mentions
+ * mv0 *)
+
+let mentions clenv mv0 = 
+  let rec menrec mv1 =
+    try
+      (match Intavm.map clenv.env mv1 with
+	 | CLVAL (b,_) -> 
+	     Intavs.memb b.freemetas mv0 or Intavs.exists menrec b.freemetas
+	 | CLTYP _ -> false)
+    with Not_found -> 
+      false
+  in 
+  menrec
+
+(* Creates a new clause-environment, whose template has a given
+ * type, CTY.  This is not all that useful, since not very often
+ * does one know the type of the clause - one usually only has
+ * a clause which one wants to backchain thru. *)
+
+let mk_clenv wc cty =
+  let mv = newMETA() in
+  let cty_fls = mk_freelisted cty in 
+  { templval = mk_freelisted(DOP0(Meta mv));
+    templtyp = cty_fls;
+    namenv = Intavm.create ();
+    env =  Intavm.add (Intavm.create ()) (mv,CLTYP cty_fls);
+    hook = wc }
+  
+let clenv_environments bound c =
+  let rec clrec (ne,e,metas) n c =
+    match n,c with
+      | (0, hd) -> (ne,e,List.rev metas,hd)
+      | (n, (DOP2(Cast,c,_))) -> clrec (ne,e,metas) n c
+      | (n, (DOP2(Prod,c1,DLAM(na,c2)))) ->
+	  let mv = newMETA() in
+	  let dep = dependent (Rel 1) c2 in
+	  let ne' =
+	    if dep then
+              (match na with
+		 | Anonymous -> ne
+		 | Name id ->
+		     if Intavm.in_dom ne mv then
+		       (warning ("Cannot put metavar "^(string_of_int mv)^
+				 " in name-environment twice");
+			ne)
+		     else Intavm.add ne (mv,id))
+            else 
+	      ne 
+	  in
+	  let e' = Intavm.add e (mv,CLTYP (mk_freelisted c1)) in 
+	  clrec (ne',e',DOP0(Meta mv)::metas) (n-1)
+	    (if dep then (subst1 (DOP0(Meta mv)) c2) else c2)
+      | (n, hd) -> (ne,e,List.rev metas,hd)
+  in 
+  clrec (Intavm.create(),Intavm.create(),[]) bound c
+
+let mk_clenv_from wc (c,cty) =
+  let (namenv,env,args,concl) = clenv_environments (-1) cty in
+  { templval = mk_freelisted (DOPN(AppL,Array.of_list (c::args)));
+    templtyp = mk_freelisted concl;
+    namenv = namenv;
+    env = env;
+    hook = wc }
+
+let connect_clenv wc clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    namenv = clenv.namenv;
+    env = clenv.env;
+    hook = wc }
+
+(* Changes the head of a clenv with (templ,templty) *)
+let clenv_change_head (templ,templty) clenv =
+  { templval = mk_freelisted templ;
+    templtyp = mk_freelisted templty;
+    namenv   = clenv.namenv;
+    env      = clenv.env;
+    hook     = clenv.hook }
+
+let mk_clenv_hnf_constr_type_of wc t =
+  mk_clenv_from wc (t,w_hnf_constr wc (w_type_of wc t))
+
+let mk_clenv_rename_from wc (c,t) = 
+  mk_clenv_from wc (c,rename_bound_var [] t)
+    
+let mk_clenv_rename_type_of wc t =
+  mk_clenv_from wc (t,rename_bound_var [] (w_type_of wc t))
+    
+let mk_clenv_rename_hnf_constr_type_of wc t =
+  mk_clenv_from wc (t,rename_bound_var [] (w_hnf_constr wc (w_type_of wc t)))
+
+let mk_clenv_type_of wc t = mk_clenv_from wc (t,w_type_of wc t)
+			      
+let mk_clenv_printable_type_of = mk_clenv_type_of
+				   
+let clenv_assign mv rhs clenv =
+  let rhs_fls = mk_freelisted rhs in 
+  if Intavs.exists (mentions clenv mv) rhs_fls.freemetas then
+    error "clenv__assign: circularity in unification";
+  try
+    (match Intavm.map clenv.env mv with
+       | CLVAL _ -> anomaly "clenv_assign: metavar already assigned"
+       | CLTYP bty -> 
+	   { templval = clenv.templval;
+	     templtyp = clenv.templtyp;
+	     namenv = clenv.namenv;
+	     env = Intavm.remap clenv.env mv (CLVAL(rhs_fls,bty));
+	     hook = clenv.hook })
+  with Not_found -> 
+    error "clenv_assign"
+
+let clenv_val_of clenv mv = 
+  let rec valrec mv =
+    try
+      (match Intavm.map clenv.env mv with
+	 | CLTYP _ -> DOP0(Meta mv)
+	 | CLVAL(b,_) ->
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
+			 (Intavs.toList b.freemetas)) b.rebus)
+    with Not_found -> 
+      DOP0(Meta mv)
+  in 
+  valrec mv
+
+let clenv_instance clenv b =
+  let c_sigma =
+    List.map (fun mv -> (mv,clenv_val_of clenv mv)) (Intavs.toList b.freemetas)
+  in 
+  instance c_sigma b.rebus
+    
+let clenv_instance_term clenv c =
+  clenv_instance clenv (mk_freelisted c)
+
+
+(* This function put casts around metavariables whose type could not be
+ * infered by the refiner, that is head of applications, predicates and
+ * subject of Cases.
+ * Does check that the casted type is closed. Anyway, the refiner would
+ * fail in this case... *)
+
+let clenv_cast_meta clenv = 
+ let rec crec u =
+   match u with
+     | DOPN((AppL|MutCase _),_)  -> crec_hd u
+     | DOP2(Cast,DOP0(Meta _),_) -> u
+     | DOPN(c,cl)                -> DOPN(c,Array.map crec cl)
+     | DOPL(c,cl)                -> DOPL(c,List.map crec cl)
+     | DOP1(c,t)                 -> DOP1(c,crec t)
+     | DOP2(c,t1,t2)             -> DOP2(c,crec t1,crec t2)
+     | DLAM(n,c)                 -> DLAM(n,crec c)
+     | DLAMV(n,cl)               -> DLAMV(n,Array.map crec cl)
+     | x                         -> x
+	   
+ and crec_hd u =
+   match kind_of_term (strip_outer_cast u) with
+     | IsMeta mv ->
+	 (try 
+	    match Intavm.map clenv.env mv with
+              | CLTYP b ->
+		  let b' = clenv_instance clenv b in 
+		  if occur_meta b' then u else mkCast u b'
+	      | CLVAL(_) -> u
+	  with Not_found -> 
+	    u)
+     | IsAppL(f,args) -> mkAppList (crec_hd f) (List.map crec args)
+     | IsMutCase(ci,p,c,br) ->
+	 mkMutCaseA ci (crec_hd p) (crec_hd c) (Array.map crec br)
+     | _ -> u
+ in 
+ crec
+
+
+(* [clenv_pose (na,mv,cty) clenv]
+ * returns a new clausenv which has added to it the metavar MV,
+ * with type CTY.  the name NA, if it is not ANONYMOUS, will
+ * be entered into the name-map, as a way of accessing the new
+ * metavar. *)
+
+let clenv_pose (na,mv,cty) clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    env = Intavm.add clenv.env (mv,CLTYP (mk_freelisted cty));
+    namenv = (match na with
+		| Anonymous -> clenv.namenv
+		| Name id -> Intavm.add clenv.namenv (mv,id));
+    hook = clenv.hook }
+
+let clenv_defined clenv mv =
+  match Intavm.map clenv.env mv with
+    | CLVAL _ -> true
+    | CLTYP _ -> false
+
+let clenv_value clenv mv =
+  match Intavm.map clenv.env mv with
+    | CLVAL(b,_) -> b
+    | CLTYP _ -> failwith "clenv_value"
+	  
+let clenv_type clenv mv =
+  match Intavm.map clenv.env mv with
+    | CLTYP b -> b
+    | CLVAL(_,b) -> b
+	  
+let clenv_template clenv = clenv.templval
+
+let clenv_template_type clenv = clenv.templtyp
+
+let clenv_instance_value clenv mv =
+  clenv_instance clenv (clenv_value clenv mv)
+    
+let clenv_instance_type clenv mv =
+  clenv_instance clenv (clenv_type clenv mv)
+    
+let clenv_instance_template clenv =
+  clenv_instance clenv (clenv_template clenv)
+    
+let clenv_instance_template_type clenv =
+  clenv_instance clenv (clenv_template_type clenv)
+    
+let clenv_wtactic wt clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    namenv = clenv.namenv;
+    env = clenv.env;
+    hook = wt clenv.hook }
+
+
+(* [clenv_unify M N clenv]
+ * performs a unification of M and N, generating a bunch of
+ * unification constraints in the process.  These constraints
+ * are processed, one-by-one - they may either generate new
+ * bindings, or, if there is already a binding, new unifications,
+ * which themselves generate new constraints.  This continues
+ * until we get failure, or we run out of constraints. *)
+
+let rec clenv_unify m n clenv =
+  let (mc,ec) = unify_0 [] clenv.hook m n in 
+  clenv_resrec mc ec clenv
+    
+and clenv_resrec metas evars clenv =
+  match (evars,metas) with
+    | ([],[]) -> clenv
+	  
+    | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
+    	clenv_resrec ((k,lhs)::metas) t clenv
+	  
+    | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) ->
+    	if w_defined_const clenv.hook evar then
+          let (metas',evars') = unify_0 [] clenv.hook rhs evar in
+          clenv_resrec (metas'@metas) (evars'@t) clenv
+    	else
+          (try 
+	     clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv)
+           with UserError _ ->
+             (match rhs with
+		| DOPN(AppL,cl) ->
+		    (match cl.(0) with
+		       | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) ->
+			   clenv_resrec metas evars 
+			     (clenv_wtactic (mimick_evar cl.(0) 
+					       ((Array.length cl) - 1) evsp) 
+				clenv)
+		       | _ -> error "w_Unify")
+           	| _ -> error "w_Unify"))
+    | ([],(mv,n)::t) ->
+    	if clenv_defined clenv mv then
+          let (metas',evars') =
+            unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
+          clenv_resrec (metas'@t) evars' clenv
+    	else 
+	  clenv_resrec t [] (clenv_assign mv n clenv)
+    | _ -> anomaly "clenv_resrec"
+	  
+
+(* [clenv_bchain mv clenv' clenv]
+ *
+ * Resolves the value of "mv" (which must be undefined) in clenv to be
+ * the template of clenv' be the value "c", applied to "n" fresh
+ * metavars, whose types are chosen by destructing "clf", which should
+ * be a clausale forme generated from the type of "c".  The process of
+ * resolution can cause unification of already-existing metavars, and
+ * of the fresh ones which get created.  This operation is a composite
+ * of operations which pose new metavars, perform unification on
+ * terms, and make bindings.  *)
+
+let clenv_bchain mv subclenv clenv =
+  (* Add the metavars of [subclenv] to [clenv], with their name-environment *)
+  let clenv' =
+    { templval = clenv.templval;
+      templtyp = clenv.templtyp;
+      namenv =
+	List.fold_left (fun ne (mv,id) ->
+			  if clenv_defined subclenv mv then 
+			    ne
+			  else if (Intavm.in_dom ne mv) then
+			    (warning ("Cannot put metavar "^(string_of_int mv)^
+				      " in name-environment twice");
+			     ne)
+			  else 
+			    Intavm.add ne (mv,id))
+          clenv.namenv (Intavm.toList subclenv.namenv);
+      env = List.fold_left Intavm.add clenv.env (Intavm.toList subclenv.env);
+      hook = clenv.hook } 
+  in
+  (* unify the type of the template of [subclenv] with the type of [mv] *)
+  let clenv'' =
+    clenv_unify (clenv_instance clenv' (clenv_template_type subclenv))
+      (clenv_instance_type clenv' mv)
+      clenv' 
+  in
+  (* assign the metavar *)
+  let clenv''' =
+    clenv_assign mv (clenv_instance clenv' (clenv_template subclenv)) clenv''
+  in 
+  clenv'''
+
+
+(* swaps the "hooks" in [clenv1] and [clenv2], so we can then use
+   backchain to hook them together *)
+
+let clenv_swap clenv1 clenv2 =
+  let clenv1' = { templval = clenv1.templval;
+		  templtyp = clenv1.templtyp;
+		  namenv = clenv1.namenv;
+		  env = clenv1.env;
+		  hook = clenv2.hook} 
+  and clenv2' = { templval = clenv2.templval;
+		  templtyp = clenv2.templtyp;
+		  namenv = clenv2.namenv;
+		  env = clenv2.env;
+		  hook = clenv1.hook}
+  in 
+  (clenv1',clenv2')
+
+let clenv_fchain mv nextclenv clenv =
+  let (clenv',nextclenv') = clenv_swap clenv nextclenv in 
+  clenv_bchain mv clenv' nextclenv'
+
+let clenv_refine kONT clenv gls =
+  tclTHEN
+    (kONT clenv.hook) 
+    (refine (clenv_instance_template clenv)) gls
+
+let clenv_refine_cast kONT clenv gls =
+  tclTHEN
+    (kONT clenv.hook) 
+    (refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
+    gls
+
+(* takes a substitution s, an open term op and a closed term cl
+   try to find a subterm of cl which matches op, if op is just a Meta
+   FAIL because we cannot find a binding *)
+
+let constrain_clenv_to_subterm clause = function 
+  | (DOP0(Meta(_)) as op),_ -> error "Match_subterm"
+  | op,cl -> 
+      let rec matchrec cl =
+    	let cl = strip_outer_cast cl in
+    	(try 
+	   if closed0 cl 
+	   then clenv_unify op cl clause,cl
+           else error "Bound 1"
+	 with UserError _ ->
+           (match telescope_appl cl with 
+	      | DOPN(AppL,tl) ->
+		  if Array.length tl = 2 then
+               	    let c1 = tl.(0) and c2 = tl.(1) in
+		    (try matchrec c1 with UserError(_) -> matchrec c2)
+		  else 
+		    error "Match_subterm"
+              | DOP2(Prod,t,DLAM(_,c)) ->
+		  (try matchrec t with UserError(_) -> matchrec c)
+              | DOP2(Lambda,t,DLAM(_,c)) ->
+		  (try matchrec t with UserError(_) -> matchrec c)
+              | _ -> error "Match_subterm")) 
+      in 
+      matchrec cl
+
+(* Possibly gives K-terms in case the operator does not contain 
+   a meta : BUG ?? *)
+let constrain_clenv_using_subterm_list allow_K clause oplist t = 
+  List.fold_right 
+    (fun op (clause,l) -> 
+       if occur_meta op then 
+         let (clause',cl) =
+           (try 
+	      constrain_clenv_to_subterm clause (strip_outer_cast op,t)
+            with (UserError _ as e) ->
+              if allow_K then (clause,op) else raise e)
+         in 
+	 (clause',cl::l)
+       else 
+	 (clause,op::l)) 
+    oplist 
+    (clause,[])
+
+(* [clenv_metavars clenv mv]
+ * returns a list of the metavars which appear in the type of
+ * the metavar mv.  The list is unordered. *)
+
+let clenv_metavars clenv mv =
+  match Intavm.map clenv.env mv with
+    | CLVAL(_,b) -> b.freemetas
+    | CLTYP b -> b.freemetas
+
+let clenv_template_metavars clenv = clenv.templval.freemetas
+
+(* [clenv_dependent clenv cval ctyp]
+ * returns a list of the metavariables which appear in the term cval,
+ * and which are dependent, This is computed by taking the metavars in cval,
+ * in right-to-left order, and collecting the metavars which appear
+ * in their types, and adding in all the metavars appearing in ctyp, the
+ * type of cval. *)
+
+let dependent_metas clenv mvs conclmetas =
+  List.fold_right
+    (fun mv deps ->
+       Intavs.union deps (clenv_metavars clenv mv))
+    mvs conclmetas
+
+let clenv_dependent clenv (cval,ctyp) =
+  let mvs = collect_metas (clenv_instance clenv cval) in
+  let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  filter (Intavs.memb deps) mvs
+
+
+(* [clenv_independent clenv (cval,ctyp)]
+ * returns a list of metavariables which appear in the term cval,
+ * and which are not dependent.  That is, they do not appear in
+ * the types of other metavars which are in cval, nor in the type
+ * of cval, ctyp. *)
+
+let clenv_independent clenv (cval,ctyp) =
+  let mvs = collect_metas (clenv_instance clenv cval) in
+  let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  filter (fun mv -> (not((Intavs.memb deps mv)))) mvs
+
+
+(* [clenv_missing clenv (cval,ctyp)]
+ * returns a list of the metavariables which appear in the term cval,
+ * and which are dependent, and do NOT appear in ctyp. *)
+
+let clenv_missing clenv (cval,ctyp) =
+  let mvs = collect_metas (clenv_instance clenv cval) in
+  let ctyp_mvs = metavars_of (clenv_instance clenv ctyp) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  filter 
+    (fun n -> Intavs.memb deps n & (not((Intavs.memb ctyp_mvs n))))
+    mvs
+
+let clenv_constrain_missing_args mlist clause =
+  if mlist = [] then 
+    clause 
+  else
+    let occlist = clenv_missing clause (clenv_template clause,
+                                   	(clenv_template_type clause)) in 
+    if List.length occlist = List.length mlist then
+      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+        clause occlist mlist
+    else 
+      error ("Not the right number of missing arguments (expected "
+	     ^(string_of_int (List.length occlist))^")")
+
+let clenv_constrain_dep_args mlist clause =
+  if mlist = [] then 
+    clause 
+  else
+    let occlist = clenv_dependent clause (clenv_template clause,
+					  (clenv_template_type clause)) in 
+    if List.length occlist = List.length mlist then
+      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+        clause occlist mlist
+    else 
+      error ("Not the right number of missing arguments (expected "
+	     ^(string_of_int (List.length occlist))^")")
+
+let clenv_constrain_dep_args_of mv mlist clause =
+  if mlist = [] then 
+    clause 
+  else
+    let occlist = clenv_dependent clause (clenv_value clause mv,
+                                          clenv_type clause mv) in 
+    if List.length occlist = List.length mlist then
+      List.fold_left2 (fun clenv occ m -> clenv_unify (DOP0(Meta occ)) m clenv)
+        clause occlist mlist
+    else 
+      error ("clenv_constrain_dep_args_of: Not the right number " ^ 
+	     "of dependent arguments")
+
+let clenv_lookup_name clenv id =
+  match Intavm.inv clenv.namenv id with
+    | []  -> 
+	errorlabstrm "clenv_lookup_name"
+          [< 'sTR"No such bound variable "; print_id id >]
+    | [n] -> 
+	n
+    |  _  -> 
+	 anomaly "clenv_lookup_name: a name occurs more than once in clause"
+
+let clenv_match_args s clause =
+  let mvs = clenv_independent clause
+	      (clenv_template clause,
+               clenv_template_type clause)
+  in 
+  let rec matchrec clause = function
+    | [] -> clause
+    | (b,c)::t ->
+	let k =
+	  (match b with
+             | Dep s ->
+		 if List.mem_assoc b t then 
+		   errorlabstrm "clenv_match_args" 
+		     [< 'sTR "The variable "; print_id s; 
+			'sTR " occurs more than once in binding" >]
+		 else 
+		   clenv_lookup_name clause s
+	     | NoDep n ->
+		 if List.mem_assoc b t then errorlabstrm "clenv_match_args"
+		   [< 'sTR "The position "; 'iNT n ;
+		      'sTR " occurs more than once in binding" >];
+		 (try 
+		    List.nth mvs (n-1)
+		  with Failure "item" -> errorlabstrm "clenv_match_args"
+                      [< 'sTR"No such binder" >])
+	     | Com -> anomaly "No free term in clenv_match_args")
+	in
+	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
+	and c_typ = w_hnf_constr clause.hook (w_type_of clause.hook c) in
+	matchrec (clenv_assign k c (clenv_unify k_typ c_typ clause)) t
+  in 
+  matchrec clause s
+
+
+(* [clenv_pose_dependent_evars clenv]
+ * For each dependent evar in the clause-env which does not have a value,
+ * pose a value for it by constructing a fresh evar.  We do this in
+ * left-to-right order, so that every evar's type is always closed w.r.t.
+ * metas.
+ *)
+let clenv_pose_dependent_evars clenv =
+  let dep_mvs = clenv_dependent clenv (clenv_template clenv,
+                                       clenv_template_type clenv) in 
+  List.fold_left
+    (fun clenv mv ->
+       let evar = new_evar_in_sign (w_hyps clenv.hook) in
+       let (evar_sp,_) = destConst evar in
+       let tY = clenv_instance_type clenv mv in
+       let tYty = w_type_of clenv.hook tY in
+       let clenv' = clenv_wtactic (w_Declare evar_sp (DOP2(Cast,tY,tYty))) 
+		      clenv in
+       clenv_assign mv evar clenv')
+    clenv
+    dep_mvs
+
+let clenv_add_sign (id,sign) clenv =
+  { templval = clenv.templval;
+    templtyp = clenv.templtyp;
+    namenv = clenv.namenv;
+    env = clenv.env;
+    hook = w_add_sign (id,sign) clenv.hook}
+
+let clenv_type_of ce c =
+  let metamap =
+    List.map 
+      (function
+	 | (n,CLVAL(_,typ)) -> (n,typ.rebus)
+         | (n,CLTYP typ)    -> (n,typ.rebus))
+      (Intavm.toList ce.env)
+  in
+  (Trad.ise_resolve true (w_Underlying ce.hook) metamap
+     (gLOB(w_hyps ce.hook)) c)._TYPE
+
+let clenv_instance_type_of ce c =
+  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+
+(* [clenv_typed_unify gls M N clenv]
+ * peforms a unification of M and N, generating a bunch of
+ * unification constraints in the process.  These constraints
+ * are processed, one-by-one - they may either generate new
+ * bindings, or, if there is already a binding, new unifications,
+ * which themselves generate new constraints.  This continues
+ * until we get failure, or we run out of constraints. *)
+
+let rec clenv_typed_unify m n clenv =
+  let (mc,ec) = unify_0 [] clenv.hook m n in 
+  clenv_resrec mc ec clenv
+
+and clenv_resrec metas evars clenv =
+  match (evars,metas) with
+    | ([],[]) -> clenv
+	  
+    | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
+    	clenv_resrec ((k,lhs)::metas) t clenv
+
+    | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) ->
+    	if w_defined_const clenv.hook evar then
+          let (metas',evars') = unify_0 [] clenv.hook rhs evar in
+          clenv_resrec (metas'@metas) (evars'@t) clenv
+    	else
+          (try 
+	     clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv)
+           with UserError _ ->
+             (match rhs with
+		| DOPN(AppL,cl) ->
+		    (match cl.(0) with
+		       | (DOPN(Const _,_) |  DOPN(MutConstruct _,_)) ->
+			   clenv_resrec metas evars 
+			     (clenv_wtactic (mimick_evar cl.(0) 
+					       ((Array.length cl) - 1) evsp) 
+				clenv)
+		       | _ -> error "w_Unify")
+           	| _ -> error "w_Unify"))
+	  
+    | ([],(mv,n)::t) ->
+    	if clenv_defined clenv mv then
+          let (metas',evars') =
+            unify_0 [] clenv.hook (clenv_value clenv mv).rebus n in
+          clenv_resrec (metas'@t) evars' clenv
+    	else 
+	  let nty = clenv_type_of clenv 
+		      (clenv_instance clenv (mk_freelisted n)) in
+	  let (mc,ec) =
+	    unify_0 [] clenv.hook (clenv_instance_type clenv mv) nty in
+	  clenv_resrec (mc@t) ec (clenv_assign mv n clenv)
+
+    | _ -> anomaly "clenv_resrec"
+
+
+(* The unique unification algorithm works like this: If the pattern is
+   flexible, and the goal has a lambda-abstraction at the head, then
+   we do a first-order unification.
+
+   If the pattern is not flexible, then we do a first-order
+   unification, too.
+
+   If the pattern is flexible, and the goal doesn't have a
+   lambda-abstraction head, then we second-order unification. *)
+
+let clenv_fo_resolver clenv gls =
+  clenv_unify (clenv_instance_template_type clenv) (pf_concl gls) clenv
+
+let clenv_typed_fo_resolver clenv gls =
+  clenv_typed_unify (clenv_instance_template_type clenv) (pf_concl gls) clenv
+
+let args_typ gls = 
+  let rec decrec l c = match pf_whd_betadeltaiota gls c with
+    | DOP2(Prod,a,DLAM(n,b)) -> decrec ((Environ.named_hd a n,a)::l) b
+    | x -> l
+  in 
+  decrec []
+
+(* if lname_type typ is [xn,An;..;x1,A1] and l is a list of terms,
+   gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
+
+let abstract_scheme c l lname_typ =
+  List.fold_left2 
+    (fun t (locc,a) (na,ta) ->
+       if occur_meta ta then error "cannot find a type for the generalisation"
+       else if occur_meta a then DOP2(Lambda,ta,DLAM(na,t))
+       else DOP2(Lambda,ta,DLAM(na,subst_term_occ locc a t)))
+    c 
+    (List.rev l)
+    lname_typ
+    
+let abstract_list_all gls typ c l =
+  let p = 
+    abstract_scheme c (List.map (function a -> [],a) l) (args_typ gls typ) in 
+  try 
+    if pf_conv_x gls (pf_type_of gls p) typ then p else 
+      error "abstract_list_all"
+  with UserError _ ->
+    let pt = pTERMINENV (gLOB (pf_hyps gls), typ) in
+    errorlabstrm "abstract_list_all"
+      [< 'sTR "cannot find a generalisation of the goal with type : "; pt >]
+
+let secondOrderAbstraction allow_K gl p oplist clause =
+  let (clause',cllist) = 
+    constrain_clenv_using_subterm_list allow_K clause oplist (pf_concl gl) in
+  let typp = clenv_instance_type clause' p in 
+  clenv_unify (DOP0(Meta p)) (abstract_list_all gl typp (pf_concl gl) cllist) 
+    clause'
+
+let clenv_so_resolver allow_K clause gl =
+  match whd_castapp_stack (clenv_instance_template_type clause) [] with
+    | (DOP0(Meta(p)),oplist) ->
+	let clause' = secondOrderAbstraction allow_K gl p oplist clause in 
+	clenv_fo_resolver clause' gl
+    | _ -> error "clenv_so_resolver"
+
+(* We decide here if first-order or second-order unif is used for Apply *)
+(* We apply a term of type (ai:Ai)C and try to solve a goal C'          *)
+(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve    *)
+
+(* 3-4-99 [HH] New fo/so choice heuristic :
+   In case we have to unify (Meta(1) args) with ([x:A]t args')
+   we first try second-order unification and if it fails first-order.
+   Before, second-order was used if the type of Meta(1) and [x:A]t was
+   convertible and first-order otherwise. But if failed if e.g. the type of
+   Meta(1) had meta-variables in it. *)
+
+let clenv_unique_resolver allow_K clenv gls =
+  match (whd_castapp_stack (clenv_instance_template_type clenv) [],
+         whd_castapp_stack (pf_concl gls) []) with
+    | ((DOP0(Meta _) as pathd,_),(DOP2(Lambda,_,_) as glhd,_)) ->
+	(try 
+	   clenv_typed_fo_resolver clenv gls
+	 with UserError (t1,t2) -> 
+	   try 
+	     clenv_so_resolver allow_K clenv gls
+	   with UserError (s1,s2) -> 
+	     error "Cannot solve a second-order unification problem")
+
+    | ((DOP0(Meta _),_),_) -> 
+	(try 
+	   clenv_so_resolver allow_K clenv gls
+         with UserError (t1,t2) -> 
+           try 
+	     clenv_typed_fo_resolver clenv gls
+           with UserError (s1,s2) -> 
+             error "Cannot solve a second-order unification problem")
+
+    | _ -> clenv_fo_resolver clenv gls
+
+
+let res_pf kONT clenv gls =
+  clenv_refine kONT (clenv_unique_resolver false clenv gls) gls
+    
+let res_pf_cast kONT clenv gls =
+  clenv_refine_cast kONT (clenv_unique_resolver false clenv gls) gls
+
+let elim_res_pf kONT clenv gls =
+  clenv_refine_cast kONT (clenv_unique_resolver true clenv gls) gls
+
+let e_res_pf kONT clenv gls =
+  clenv_refine kONT
+    (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
new file mode 100644
index 0000000000..b5675f1a12
--- /dev/null
+++ b/proofs/clenv.mli
@@ -0,0 +1,95 @@
+
+(* $Id$ *)
+
+(*i*)
+open Util
+open Names
+open Term
+open Tacmach
+open Proof_trees
+(*i*)
+
+(* The Type of Constructions clausale environments. *)
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Intset.t }
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Intmap.t;
+  env : clbinding Intmap.t;
+  hook : 'a }
+
+(* templval is the template which we are trying to fill out.
+ * templtyp is its type.
+ * namenv is a mapping from metavar numbers to names, for
+ *        use in instanciating metavars by name.
+ * env is the mapping from metavar numbers to their types
+ *     and values.
+ * hook is the pointer to the current walking context, for
+ *      integrating existential vars and metavars.
+ *)
+
+type wc = walking_constraints (* Pour une meilleure lisibilité *)
+
+val unify : constr -> tactic
+val unify_0 : 
+  (int * constr) list -> wc -> constr -> constr 
+    -> (int * constr) list * (constr * constr) list
+
+val collect_metas : constr -> int list
+val mk_clenv : 'a -> constr -> 'a clausenv
+val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
+val mk_clenv_rename_from : 'a -> constr * constr -> 'a clausenv
+val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
+val mk_clenv_printable_type_of : wc -> constr -> wc clausenv
+val mk_clenv_type_of : wc -> constr -> wc clausenv
+
+val connect_clenv : wc -> 'a clausenv -> wc clausenv
+val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
+val clenv_assign : int -> constr -> 'a clausenv -> 'a clausenv
+val clenv_instance_term : 'a clausenv -> constr -> constr
+val clenv_pose : name * int * constr -> 'a clausenv -> 'a clausenv
+val clenv_template : 'a clausenv -> constr freelisted
+val clenv_template_type : 'a clausenv -> constr freelisted
+val clenv_instance_type : 'a clausenv -> int -> constr
+val clenv_instance_template : 'a clausenv -> constr
+val clenv_instance_template_type : 'a clausenv -> constr
+val clenv_unify : constr -> constr -> wc clausenv -> wc clausenv
+val clenv_fchain : int -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
+val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
+val elim_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val clenv_independent : 
+  'a clausenv -> constr freelisted * constr freelisted -> int list
+val clenv_missing : 
+  'a clausenv -> constr freelisted * constr freelisted -> int list
+val clenv_constrain_missing_args : constr list -> wc clausenv -> wc clausenv
+val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
+val clenv_lookup_name : 'a clausenv -> identifier -> int
+val clenv_match_args : (bindOcc * constr) list -> wc clausenv -> wc clausenv
+val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
+
+(* [abstract_list_all sig c t l]                           *)
+(* abstracts the terms in l over c to get a term of type t *)
+val abstract_list_all : goal sigma -> constr -> constr -> constr list -> constr
+
+(* Exported for program.ml only *)
+val clenv_add_sign : 
+  (identifier * typed_type) -> wc clausenv -> wc clausenv
+val constrain_clenv_to_subterm : 
+  wc clausenv -> constr * constr -> wc clausenv * constr
+val clenv_constrain_dep_args_of : 
+  int -> constr list -> wc clausenv -> wc clausenv
+val constrain_clenv_using_subterm_list : 
+  bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
+val clenv_typed_unify : constr -> constr -> wc clausenv -> wc clausenv
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a52e8603d1..21bfb2d71e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -20,9 +20,13 @@ type refiner_error =
   | BadType of constr * constr * constr
   | OccurMeta of constr
   | CannotApply of constr * constr
+  | CannotUnify of constr * constr
 
 exception RefinerError of refiner_error
 
+let error_cannot_unify k (m,n) =
+  raise (RefinerError (CannotUnify (m,n)))
+
 let conv_leq_goal env sigma arg ty conclty =
   if not (is_conv_leq env sigma ty conclty) then 
     raise (RefinerError (BadType (arg,ty,conclty)))
diff --git a/proofs/logic.mli b/proofs/logic.mli
index cbab2a90ca..cbd94b52b1 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -2,6 +2,7 @@
 (* $Id$ *)
 
 (*i*)
+open Names
 open Term
 open Sign
 open Evd
@@ -9,6 +10,8 @@ open Environ
 open Proof_trees
 (*i*)
 
+(* The primitive refiner. *)
+
 val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
@@ -16,3 +19,14 @@ val prim_extractor :
     (typed_type, constr) env -> proof_tree -> constr
 
 val extract_constr : constr assumptions -> constr -> constr
+
+
+(*s Refiner errors. *)
+
+type refiner_error =
+  | BadType of constr * constr * constr
+  | OccurMeta of constr
+  | CannotApply of constr * constr
+  | CannotUnify of constr * constr
+
+val error_cannot_unify : path_kind -> constr * constr -> 'a
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c4c8dc6ed2..a889e668c9 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -2,22 +2,21 @@
 (* $Id$ *)
 
 open Util
+open Stamps
 open Names
 open Generic
-open Evd
+open Sign
 open Term
+open Instantiate
+open Environ
 open Reduction
-open Himsg
-open Termenv
-open Termast
-open CoqAst
-open Trad
+open Evd
+open Typing_ev
+open Tacred
 open Proof_trees
-open Printer
-
 open Logic
-open Evar_refiner
 open Refiner
+open Evar_refiner
 
 
 type 'a sigma = 'a Refiner.sigma
@@ -37,59 +36,43 @@ let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
 
-let sig_it       = Refiner.sig_it
-let sig_sig      = Refiner.sig_sig
-let project      = (comp ts_it sig_sig)
-let pf_hyps gls  = (sig_it gls).hyps
+let sig_it     = Refiner.sig_it
+let sig_sig    = Refiner.sig_sig
+let project    = compose ts_it sig_sig
+let pf_env gls = (sig_it gls).evar_env
 
-let pf_untyped_hyps gls  =
-  let (idl,tyl) = (sig_it gls).hyps in (idl, List.map (fun x -> x.body) tyl)
+let pf_concl gls = (sig_it gls).evar_concl
 
-let pf_concl gls = (sig_it gls).concl
+let pf_untyped_hyps gls  =
+  let env = pf_env gls in
+  let (idl,tyl) = get_globals (Environ.context env) in 
+  (idl, List.map (fun x -> x.body) tyl)
 
 let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
 
 let pf_get_hyp gls id = 
-  try (snd (lookup_sign id (pf_untyped_hyps gls)))
-  with Not_found -> error ("No such hypothesis : " ^ (string_of_id id))
+  try 
+    snd (lookup_sign id (pf_untyped_hyps gls))
+  with Not_found -> 
+    error ("No such hypothesis : " ^ (string_of_id id))
 
 let pf_ctxt gls      = get_ctxt (sig_it gls)
 
 let pf_type_of gls c =
-  Mach.type_of (ts_it (sig_sig gls)) (sig_it gls).hyps c
+  type_of (sig_it gls).evar_env (ts_it (sig_sig gls)) c
 
 let hnf_type_of gls = 
-  (comp (whd_betadeltaiota (project gls)) (pf_type_of gls))
+  compose 
+    (whd_betadeltaiota (sig_it gls).evar_env (project gls)) 
+    (pf_type_of gls)
 
 let pf_check_type gls c1 c2 =
   let casted = mkCast c1 c2 in pf_type_of gls casted
 
-let pf_constr_of_com gls c =
-  let evc = project gls in 
-  constr_of_com evc (sig_it gls).hyps c
-
-let pf_constr_of_com_sort gls c =
-  let evc = project gls in 
-  constr_of_com_sort evc (sig_it gls).hyps c
-
-let pf_global gls id = Machops.global (gLOB (sig_it gls).hyps) id
-let pf_parse_const gls = comp (pf_global gls) id_of_string 
-
-			   
-(* We sould not call Mach in tactics *)
-let pf_fexecute gls =
-  let evc = project gls in 
-  Trad.ise_resolve true evc [] (gLOB (sig_it gls).hyps)
-
-let pf_infexecute gls =
-  let evc = project gls in
-  let sign = (sig_it gls).hyps in 
-  Mach.infexecute evc (sign, Mach.fsign_of_sign evc sign)
-
 let pf_reduction_of_redexp gls re c = 
-  reduction_of_redexp re (project gls) c 
+  reduction_of_redexp re (pf_env gls) (project gls) c 
 
-let pf_reduce redfun gls c       = redfun (project gls) c 
+let pf_reduce redfun gls c       = redfun (pf_env gls) (project gls) c 
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
 let pf_hnf_constr                = pf_reduce hnf_constr
@@ -98,9 +81,9 @@ let pf_nf                        = pf_reduce nf
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 
-let pf_conv_x                   = pf_reduce conv_x
-let pf_conv_x_leq               = pf_reduce conv_x_leq
-let pf_const_value              = pf_reduce const_value
+let pf_conv_x                   = pf_reduce conv
+let pf_conv_x_leq               = pf_reduce conv_leq
+let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_one_step_reduce          = pf_reduce one_step_reduce
 let pf_reduce_to_mind           = pf_reduce reduce_to_mind
 let pf_reduce_to_ind            = pf_reduce reduce_to_ind
@@ -169,18 +152,18 @@ let w_Declare       = w_Declare
 let w_Declare_At    = w_Declare_At
 let w_Define        = w_Define
 let w_Underlying    = w_Underlying
-let w_hyps          = w_hyps
+let w_env           = w_env
 let w_type_of       = w_type_of
 let w_IDTAC         = w_IDTAC
 let w_ORELSE        = w_ORELSE
 let w_add_sign      = w_add_sign
 let ctxt_type_of    = ctxt_type_of
 
-let w_defined_const wc k     = defined_const (w_Underlying wc) k
-let w_const_value wc         = const_value (w_Underlying wc)
-let w_conv_x wc m n          = conv_x (w_Underlying wc) m n
-let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_Underlying wc) c
-let w_hnf_constr wc c         = hnf_constr (w_Underlying wc) c
+let w_defined_const wc k     = defined_constant (w_env wc) k
+let w_const_value wc         = constant_value (w_env wc)
+let w_conv_x wc m n          = conv (w_env wc) (w_Underlying wc) m n
+let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
+let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 
 
 (*************************************************)
@@ -205,8 +188,7 @@ let tclFAIL          =  tclFAIL
 let tclDO            =  tclDO
 let tclPROGRESS      =  tclPROGRESS
 let tclWEAK_PROGRESS = tclWEAK_PROGRESS
-let tclNOTSAMEGOAL = tclNOTSAMEGOAL
-let tclINFO          =  tclINFO
+let tclNOTSAMEGOAL   = tclNOTSAMEGOAL
 
 let unTAC            = unTAC
 
@@ -230,37 +212,37 @@ let refine c pf =
 		  hypspecs = []; newids = []; params = [] }) pf
 
 let convert_concl c pf = 
-  refiner (PRIM{name=CONVERT_CONCL;terms=[c];
-                hypspecs=[];newids=[];params=[]}) pf
+  refiner (Prim { name = Convert_concl; terms = [c];
+                  hypspecs = []; newids = []; params = [] }) pf
 
 let convert_hyp id c pf = 
-  refiner (PRIM{name=CONVERT_HYP;hypspecs=[id];
-                terms=[c];newids=[];params=[]}) pf
+  refiner (Prim { name = Convert_hyp; hypspecs = [id];
+                  terms = [c]; newids = []; params = []}) pf
 
 let thin ids gl = 
-  refiner (PRIM{name=THIN;hypspecs=ids;
-                terms=[];newids=[];params=[]}) gl
+  refiner (Prim { name = Thin; hypspecs = ids;
+                  terms = []; newids = []; params = []}) gl
 
 let move_hyp with_dep id1 id2 gl = 
-  refiner (PRIM{name=MOVE with_dep;
-                hypspecs=[id1;id2];terms=[];newids=[];params=[]}) gl
+  refiner (Prim { name = Move with_dep;
+                  hypspecs = [id1;id2]; terms = [];
+		  newids = []; params = []}) gl
 
 let mutual_fix lf ln lar pf = 
-  refiner (PRIM{name=FIX;newids=lf;
-                hypspecs=[];terms=lar;
-                params=List.map num ln}) pf
+  refiner (Prim { name = Fix; newids = lf;
+                  hypspecs = []; terms = lar;
+                  params = List.map Ast.num ln}) pf
 
 let mutual_cofix lf lar pf = 
-  refiner (PRIM{name     = COFIX;
-                newids   = lf;
-                hypspecs = [];
-                terms    = lar; 
-                params   = []}) pf
+  refiner (Prim { name     = Cofix;
+                  newids   = lf; hypspecs = [];
+                  terms    = lar; params   = []}) pf
     
 let rename_bound_var_goal gls =
-  let ({hyps=sign;concl=cl} as gl) = (sig_it gls) in 
-  convert_concl (rename_bound_var (ids_of_sign sign) cl) gls
-
+  let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
+  let ids = ids_of_sign (get_globals (Environ.context env)) in
+  convert_concl (rename_bound_var ids cl) gls
+    
 
 (***************************************)
 (* The interpreter of defined tactics *)
@@ -269,42 +251,6 @@ let rename_bound_var_goal gls =
 let vernac_tactic = vernac_tactic
 let context       = context
 
-
-(************************************************************************)
-(* A generic tactic registration function with a default tactic printer *)
-(************************************************************************)
-
-(* A generic tactic printer *)
-
-let pr_com sigma goal com =
-  prterm (rename_bound_var 
-            (ids_of_sign goal.hyps) 
-            (Trad.constr_of_com sigma goal.hyps com))
-    
-let pr_one_binding sigma goal = function
-  | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]
-  | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >]
-  | (Com,com)     -> [< pr_com sigma goal com >]
-
-let pr_bindings sigma goal lb =
-  let prf = pr_one_binding sigma goal in 
-  match lb with 
-    | [] -> [< prlist_with_sep pr_spc prf lb >]
-    | _  -> [<'sTR"with";'sPC;prlist_with_sep pr_spc prf lb >]
-
-let rec pr_list f = function
-  | []   -> [<>] 
-  | a::l1 -> [< (f a) ; pr_list f l1>]
-
-let pr_gls gls =
-  hOV 0 [< pr_decls (sig_sig gls) ; 'fNL ; pr_seq (sig_it gls) >]
-
-let pr_glls glls =
-  hOV 0 [< pr_decls (sig_sig glls) ; 'fNL ;
-           prlist_with_sep pr_fnl pr_seq (sig_it glls) >]
-
-let pr_tactic = Refiner.pr_tactic
-
 let add_tactic = Refiner.add_tactic
 
 let overwriting_tactic = Refiner.overwriting_add_tactic
@@ -323,11 +269,6 @@ let overwrite_hidden_tactic s tac  =
   overwriting_add_tactic s tac;
   (fun args -> vernac_tactic(s,args))
 
-(* Some combinators for parsing tactic arguments. 
-   They transform the CoqAst.t arguments of the tactic into 
-   constr arguments *)
-
-type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
 
 let tactic_com = 
   fun tac t x -> tac (pf_constr_of_com x t) x
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 1d03b5c938..07a7be00c7 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -28,9 +28,10 @@ val repackage : global_constraints ref -> 'a -> 'a sigma
 val apply_sig_tac :
   global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
 
+val pf_concl              : goal sigma -> constr
 val pf_env                : goal sigma -> unsafe_env
+val pf_hyps               : goal sigma -> typed_type signature
 val pf_untyped_hyps       : goal sigma -> constr signature
-val pf_concl              : goal sigma -> constr
 val pf_nth_hyp            : goal sigma -> int -> identifier * constr
 val pf_ctxt               : goal sigma -> ctxtty
 val pf_global             : goal sigma -> identifier -> constr
@@ -174,6 +175,7 @@ val w_Declare           : section_path -> constr -> w_tactic
 val w_Declare_At        : section_path -> section_path -> constr -> w_tactic
 val w_Define            : section_path -> constr -> w_tactic
 val w_Underlying        : walking_constraints -> evar_declarations
+val w_env               : walking_constraints -> unsafe_env
 val w_hyps              : walking_constraints -> context
 val w_type_of           : walking_constraints -> constr -> constr
 val w_add_sign          : (identifier * typed_type) 
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
index e965816c7b..f932cf66ed 100644
--- a/proofs/tacred.mli
+++ b/proofs/tacred.mli
@@ -4,11 +4,24 @@
 (*i*)
 open Names
 open Term
+open Environ
+open Evd
 open Reduction
 (*i*)
 
 (* Reduction functions associated to tactics. *)
 
+val hnf_constr : 'a reduction_function
+
+val nf : 'a reduction_function
+
+val one_step_reduce : 'a reduction_function
+
+val reduce_to_mind : 
+  unsafe_env -> 'a evar_map -> constr -> constr * constr * constr
+val reduce_to_ind : 
+  unsafe_env -> 'a evar_map -> constr -> section_path * constr * constr
+
 type red_expr =
   | Red
   | Hnf