Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 1175 insertions, 0 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
new file mode 100644
index 00000000..423350d7
--- /dev/null
+++ b/proofs/clenv.ml
@@ -0,0 +1,1175 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: clenv.ml,v 1.97.2.3 2004/07/16 19:30:48 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Instantiate
+open Environ
+open Evd
+open Proof_type
+open Refiner
+open Proof_trees
+open Logic
+open Reductionops
+open Tacmach
+open Evar_refiner
+open Rawterm
+open Pattern
+open Tacexpr
+
+(* if lname_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 env c l lname_typ =
+  List.fold_left2 
+    (fun t (locc,a) (na,_,ta) ->
+       let na = match kind_of_term a with Var id -> Name id | _ -> na in
+       if occur_meta ta then error "cannot find a type for the generalisation"
+       else if occur_meta a then lambda_name env (na,ta,t)
+       else lambda_name env (na,ta,subst_term_occ locc a t))
+    c
+    (List.rev l)
+    lname_typ
+
+let abstract_list_all env sigma typ c l =
+  let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in
+  let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in 
+  try 
+    if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p
+    else error "abstract_list_all"
+  with UserError _ ->
+    raise (RefinerError (CannotGeneralize typ))
+
+(* Generator of metavariables *)
+let new_meta =
+  let meta_ctr = ref 0 in
+  fun () -> incr meta_ctr; !meta_ctr
+
+(* replaces a mapping of existentials into a mapping of metas.
+   Problem if an evar appears in the type of another one (pops anomaly) *)
+let exist_to_meta sigma (emap, c) =
+  let metamap = ref [] in
+  let change_exist evar =
+    let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+    let n = new_meta() in
+    metamap := (n, ty) :: !metamap;
+    mkMeta n in
+  let rec replace c =
+    match kind_of_term c with
+        Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev
+      | _ -> map_constr replace c in
+  (!metamap, replace c)
+
+module Metaset = Intset
+
+module Metamap = Intmap
+
+let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false
+
+let metamap_in_dom x m =
+  try let _ = Metamap.find x m in true with Not_found -> false
+
+let metamap_to_list m =
+  Metamap.fold (fun n v l -> (n,v)::l) m []
+
+let metamap_inv m b = 
+  Metamap.fold (fun n v l -> if v = b then n::l else l) m []
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+(* collects all metavar occurences, in left-to-right order, preserving
+ * repetitions and all. *)
+
+let collect_metas c = 
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> mv::acc
+      | _         -> fold_constr collrec acc c
+  in
+  List.rev (collrec [] c)
+
+let metavars_of c =  
+  let rec collrec acc c =
+    match kind_of_term c with
+      | Meta mv -> Metaset.add mv acc
+      | _         -> fold_constr collrec acc c
+  in 
+  collrec Metaset.empty c
+
+let mk_freelisted c =
+  { rebus = c; freemetas = metavars_of c }
+
+
+(* Clausal environments *)
+
+type clbinding = 
+  | Cltyp of constr freelisted
+  | Clval of constr freelisted * constr freelisted
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Metamap.t;
+  env : clbinding Metamap.t;
+  hook : 'a }
+
+type wc = named_context sigma
+
+
+(* [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 Metamap.find mv1 clenv.env with
+	 | Clval (b,_) -> 
+	     Metaset.mem mv0 b.freemetas || meta_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 = new_meta () in
+  let cty_fls = mk_freelisted cty in 
+  { templval = mk_freelisted (mkMeta mv);
+    templtyp = cty_fls;
+    namenv = Metamap.empty;
+    env =  Metamap.add mv (Cltyp cty_fls) Metamap.empty ;
+    hook = wc }
+  
+let clenv_environments bound c =
+  let rec clrec (ne,e,metas) n c =
+    match n, kind_of_term c with
+      | (Some 0, _) -> (ne, e, List.rev metas, c)
+      | (n, Cast (c,_)) -> clrec (ne,e,metas) n c
+      | (n, Prod (na,c1,c2)) ->
+	  let mv = new_meta () in
+	  let dep = dependent (mkRel 1) c2 in
+	  let ne' =
+	    if dep then
+              match na with
+		| Anonymous -> ne
+		| Name id ->
+		    if metamap_in_dom mv ne then begin
+		      warning ("Cannot put metavar "^(string_of_meta mv)^
+			       " in name-environment twice");
+		      ne
+		    end else 
+		      Metamap.add mv id ne
+            else 
+	      ne 
+	  in
+	  let e' = Metamap.add mv (Cltyp (mk_freelisted c1)) e in 
+	  clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+	    (if dep then (subst1 (mkMeta mv) c2) else c2)
+      | (n, LetIn (na,b,_,c)) ->
+	  clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+      | (n, _) -> (ne, e, List.rev metas, c)
+  in 
+  clrec (Metamap.empty,Metamap.empty,[]) bound c
+
+let mk_clenv_from_n wc n (c,cty) =
+  let (namenv,env,args,concl) = clenv_environments n cty in
+  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
+    templtyp = mk_freelisted concl;
+    namenv = namenv;
+    env = env;
+    hook = wc }
+
+let mk_clenv_from wc = mk_clenv_from_n wc None
+
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
+let map_clb f = function
+  | Cltyp cfl -> Cltyp (map_fl f cfl)
+  | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2)
+
+let subst_clenv f sub clenv = 
+  { templval = map_fl (subst_mps sub) clenv.templval;
+    templtyp = map_fl (subst_mps sub) clenv.templtyp;
+    namenv = clenv.namenv;
+    env = Metamap.map (map_clb (subst_mps sub)) clenv.env;
+    hook = f sub clenv.hook }
+
+let connect_clenv wc clenv = { clenv with hook = wc }
+
+(* Was used in wcclausenv.ml
+(* 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 (w_env wc) [] t)
+
+let mk_clenv_rename_from_n wc n (c,t) = 
+  mk_clenv_from_n wc n (c,rename_bound_var (w_env wc) [] t)
+    
+let mk_clenv_rename_type_of wc t =
+  mk_clenv_from wc (t,rename_bound_var (w_env wc) [] (w_type_of wc t))
+    
+let mk_clenv_rename_hnf_constr_type_of wc t =
+  mk_clenv_from wc
+    (t,rename_bound_var (w_env wc) [] (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 clenv_assign mv rhs clenv =
+  let rhs_fls = mk_freelisted rhs in 
+  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
+    error "clenv__assign: circularity in unification";
+  try
+    (match Metamap.find mv clenv.env with
+       | Clval (fls,ty) ->
+	   if not (eq_constr fls.rebus rhs) then
+	     try 
+	       (* Streams are lazy, force evaluation of id to catch Not_found*)
+	       let id = Metamap.find mv clenv.namenv in
+	       errorlabstrm "clenv_assign"
+		 (str "An incompatible instantiation has already been found for " ++ 
+		    pr_id id)
+	     with Not_found ->
+	       anomaly "clenv_assign: non dependent metavar already assigned"
+	   else
+	     clenv
+       | Cltyp bty -> 
+	   { templval = clenv.templval;
+	     templtyp = clenv.templtyp;
+	     namenv = clenv.namenv;
+	     env = Metamap.add mv (Clval (rhs_fls,bty)) clenv.env;
+	     hook = clenv.hook })
+  with Not_found -> 
+    error "clenv_assign"
+
+let clenv_val_of clenv mv = 
+  let rec valrec mv =
+    try
+      (match Metamap.find mv clenv.env with
+	 | Cltyp _ -> mkMeta mv
+	 | Clval(b,_) ->
+	     instance (List.map (fun mv' -> (mv',valrec mv')) 
+			       (Metaset.elements b.freemetas)) b.rebus)
+    with Not_found -> 
+      mkMeta mv
+  in 
+  valrec mv
+
+let clenv_instance clenv b =
+  let c_sigma =
+    List.map 
+      (fun mv -> (mv,clenv_val_of clenv mv)) (Metaset.elements 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 kind_of_term u with
+      | App _ | Case _ -> crec_hd u
+      | Cast (c,_) when isMeta c -> u
+      | _  -> map_constr crec u
+	    
+  and crec_hd u =
+    match kind_of_term (strip_outer_cast u) with
+      | Meta mv ->
+	  (try 
+	     match Metamap.find mv clenv.env with
+               | Cltyp b ->
+		   let b' = clenv_instance clenv b in 
+		   if occur_meta b' then u else mkCast (mkMeta mv, b')
+	       | Clval(_) -> u
+	   with Not_found -> 
+	     u)
+      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+      | Case(ci,p,c,br) ->
+	  mkCase (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 = Metamap.add mv (Cltyp (mk_freelisted cty)) clenv.env;
+    namenv = (match na with
+		| Anonymous -> clenv.namenv
+		| Name id -> Metamap.add mv id clenv.namenv);
+    hook = clenv.hook }
+
+let clenv_defined clenv mv =
+  match Metamap.find mv clenv.env with
+    | Clval _ -> true
+    | Cltyp _ -> false
+
+let clenv_value clenv mv =
+  match Metamap.find mv clenv.env with
+    | Clval(b,_) -> b
+    | Cltyp _ -> failwith "clenv_value"
+	  
+let clenv_type clenv mv =
+  match Metamap.find mv clenv.env 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 }
+
+let clenv_type_of ce c =
+  let metamap =
+    List.map 
+      (function
+	 | (n,Clval(_,typ)) -> (n,typ.rebus)
+         | (n,Cltyp typ)    -> (n,typ.rebus))
+      (metamap_to_list ce.env)
+  in
+    Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c
+
+let clenv_instance_type_of ce c =
+  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+
+
+
+(* 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 *)
+
+(* Unification order: *)
+(* Left to right: unifies first argument and then the other arguments *)
+(*let unify_l2r x = List.rev x
+(* Right to left: unifies last argument and then the other arguments *)
+let unify_r2l x = x
+
+let sort_eqns = unify_r2l
+*)
+
+let unify_0 cv_pb wc m n =
+  let env = w_env wc
+  and sigma = w_Underlying wc in
+  let trivial_unify pb substn m n =
+    if (not(occur_meta m)) & is_fconv pb env sigma m n then substn
+    else error_cannot_unify (m,n) in
+  let rec unirec_rec pb ((metasubst,evarsubst) as substn) m n =
+    let cM = Evarutil.whd_castappevar sigma m
+    and cN = Evarutil.whd_castappevar sigma n in 
+    match (kind_of_term cM,kind_of_term cN) with
+      | Meta k1, Meta k2 ->
+	  if k1 < k2 then (k1,cN)::metasubst,evarsubst
+	  else if k1 = k2 then substn
+	  else (k2,cM)::metasubst,evarsubst
+      | Meta k, _    -> (k,cN)::metasubst,evarsubst
+      | _, Meta k    -> (k,cM)::metasubst,evarsubst
+      | Evar _, _ -> metasubst,((cM,cN)::evarsubst)
+      | _, Evar _ -> metasubst,((cN,cM)::evarsubst)
+
+      | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
+	  unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2
+      | Prod (_,t1,c1), Prod (_,t2,c2) ->
+	  unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2
+      | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN
+      | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c)
+
+      | App (f1,l1), App (f2,l2) ->
+	  let len1 = Array.length l1
+	  and len2 = Array.length l2 in
+          let (f1,l1,f2,l2) =
+	    if len1 = len2 then (f1,l1,f2,l2)
+	    else if len1 < len2 then
+              let extras,restl2 = array_chop (len2-len1) l2 in 
+              (f1, l1, appvect (f2,extras), restl2)
+	    else 
+	      let extras,restl1 = array_chop (len1-len2) l1 in 
+              (appvect (f1,extras), restl1, f2, l2) in
+          (try
+            array_fold_left2 (unirec_rec CONV)
+	      (unirec_rec CONV substn f1 f2) l1 l2
+	  with ex when catchable_exception ex ->
+            trivial_unify pb substn cM cN)
+      | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
+          array_fold_left2 (unirec_rec CONV)
+	    (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2
+
+      | _ -> trivial_unify pb substn cM cN
+
+  in
+  if (not(occur_meta m)) & is_fconv cv_pb env sigma m n then 
+    ([],[])
+  else 
+    let (mc,ec) = unirec_rec cv_pb ([],[]) m n in
+    ((*sort_eqns*) mc, (*sort_eqns*) ec)
+
+
+(* 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 applyHead n c wc = 
+  let rec apprec n c cty wc =
+    if n = 0 then 
+      (wc,c)
+    else 
+      match kind_of_term (w_whd_betadeltaiota wc cty) with
+        | Prod (_,c1,c2) ->
+	    let evar = Evarutil.new_evar_in_sign (w_env wc) in
+            let (evar_n, _) = destEvar evar in
+	    (compose 
+	       (apprec (n-1) (applist(c,[evar])) (subst1 evar c2))
+	       (w_Declare evar_n c1))
+	    wc
+	| _ -> error "Apply_Head_Then"
+  in 
+  apprec n c (w_type_of wc c) wc
+
+let is_mimick_head f =
+  match kind_of_term f with
+      (Const _|Var _|Rel _|Construct _|Ind _) -> true
+    | _ -> false
+
+let rec mimick_evar hdc nargs sp wc =
+  let evd = Evd.map wc.sigma sp in
+  let wc' = extract_decl sp wc in
+  let (wc'', c) = applyHead nargs hdc wc' in
+  let (mc,ec) = unify_0 CONV wc'' (w_type_of wc'' c) (evd.evar_concl) in
+  let (wc''',_) = w_resrec mc ec wc'' in
+    if wc'== wc'''
+    then w_Define sp c wc
+    else  
+      let wc'''' = restore_decl sp evd wc''' in
+	w_Define sp (Evarutil.nf_evar wc''''.sigma c) {it = wc.it ; sigma = wc''''.sigma}
+
+and w_Unify cv_pb m n wc =
+  let (mc',ec') = unify_0 cv_pb wc m n in 
+  w_resrec mc' ec' wc
+
+and w_resrec metas evars wc =
+  match evars with
+    | [] -> (wc,metas)
+
+    | (lhs,rhs) :: t ->
+    match kind_of_term rhs with
+
+      | Meta k -> w_resrec ((k,lhs)::metas) t wc
+
+      | krhs ->
+      match kind_of_term lhs with
+
+	| Evar (evn,_) ->
+	    if w_defined_evar wc evn then
+	      let (wc',metas') = w_Unify CONV rhs lhs wc in 
+	      w_resrec (metas@metas') t wc'
+	    else
+	      (try 
+		 w_resrec metas t (w_Define evn rhs wc)
+               with ex when catchable_exception ex ->
+		 (match krhs with
+             	    | App (f,cl) when is_mimick_head f ->
+			let wc' = mimick_evar f (Array.length cl) evn wc in
+			w_resrec metas evars wc'
+		    | _ -> raise ex (*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 CONV m n [] wc)) *)
+let unifyTerms m n gls = 
+  tclIDTAC {it = gls.it; 
+	    sigma = (get_gc (fst (w_Unify CONV m n (Refiner.project_with_focus gls))))}
+
+let unify m gls =
+  let n = pf_concl gls in unifyTerms m n gls
+
+(* [clenv_merge b metas evars clenv] merges common instances in metas
+   or in evars, possibly generating new unification problems; if [b]
+   is true, unification of types of metas is required *)
+
+let clenv_merge with_types metas evars clenv =
+  let ty_metas = ref [] in
+  let ty_evars = ref [] in
+  let rec clenv_resrec metas evars clenv =
+    match (evars,metas) with
+      | ([], []) -> clenv
+
+      | ((lhs,rhs)::t, metas) ->
+      (match kind_of_term rhs with
+
+	| Meta k -> clenv_resrec ((k,lhs)::metas) t clenv
+
+	| krhs ->
+        (match kind_of_term lhs with
+
+	  | Evar (evn,_) ->
+    	      if w_defined_evar clenv.hook evn then
+		let (metas',evars') = unify_0 CONV clenv.hook rhs lhs in
+		clenv_resrec (metas'@metas) (evars'@t) clenv
+    	      else begin
+		let rhs' = 
+		  if occur_meta rhs then subst_meta metas rhs else rhs 
+		in
+		if occur_evar evn rhs' then error "w_Unify";
+		try 
+		  clenv_resrec metas t 
+		    (clenv_wtactic (w_Define evn rhs') clenv) 
+		with ex when catchable_exception ex ->
+		  (match krhs with
+		     | App (f,cl) when is_mimick_head f ->
+			 clenv_resrec metas evars 
+			   (clenv_wtactic
+			      (mimick_evar f (Array.length cl) evn)
+			      clenv)
+           	     | _ -> raise ex (********* error "w_Unify" *))
+	      end
+
+	  | _ -> anomaly "clenv_resrec"))
+
+      | ([], (mv,n)::t) ->
+    	  if clenv_defined clenv mv then
+            let (metas',evars') =
+              unify_0 CONV clenv.hook (clenv_value clenv mv).rebus n in
+            clenv_resrec (metas'@t) evars' clenv
+    	  else
+            begin
+	      if with_types (* or occur_meta mvty *) then
+	        (let mvty = clenv_instance_type clenv mv in
+		try 
+		  let nty = clenv_type_of clenv 
+			      (clenv_instance clenv (mk_freelisted n)) in
+		  let (mc,ec) = unify_0 CUMUL clenv.hook nty mvty in
+                  ty_metas := mc @ !ty_metas;
+                  ty_evars := ec @ !ty_evars
+		with e when Logic.catchable_exception e -> ());
+	      clenv_resrec t [] (clenv_assign mv n clenv)
+            end in
+  (* merge constraints *)
+  let clenv' = clenv_resrec metas evars clenv in
+  if with_types then
+    (* merge constraints about types: if they fail, don't worry *)
+    try clenv_resrec !ty_metas !ty_evars clenv'
+    with e when Logic.catchable_exception e -> clenv'
+  else clenv'
+
+(* [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.
+   [clenv_typed_unify M N clenv] expects in addition that expected
+   types of metavars are unifiable with the types of their instances    *)
+
+let clenv_unify_core_0 with_types cv_pb m n clenv =
+  let (mc,ec) = unify_0 cv_pb clenv.hook m n in 
+  clenv_merge with_types mc ec clenv
+
+let clenv_unify_0 = clenv_unify_core_0 false
+let clenv_typed_unify = clenv_unify_core_0 true
+
+
+(* 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 iter_fail f a =
+  let n = Array.length a in 
+  let rec ffail i =
+    if i = n then error "iter_fail" 
+    else
+      try f a.(i) 
+      with ex when catchable_exception ex -> ffail (i+1)
+  in ffail 0
+
+(* Tries to find an instance of term [cl] in term [op].
+   Unifies [cl] to every subterm of [op] until it finds a match.
+   Fails if no match is found *)
+let unify_to_subterm clause (op,cl) =
+  let rec matchrec cl =
+    let cl = strip_outer_cast cl in
+    (try 
+       if closed0 cl 
+       then clenv_unify_0 CONV op cl clause,cl
+       else error "Bound 1"
+     with ex when catchable_exception ex ->
+       (match kind_of_term cl with 
+	  | App (f,args) ->
+	      let n = Array.length args in
+	      assert (n>0);
+	      let c1 = mkApp (f,Array.sub args 0 (n-1)) in
+	      let c2 = args.(n-1) in
+	      (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+          | Case(_,_,c,lf) -> (* does not search in the predicate *)
+	       (try 
+		 matchrec c
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec lf)
+	  | LetIn(_,c1,_,c2) -> 
+	       (try 
+		 matchrec c1
+	       with ex when catchable_exception ex -> 
+		 matchrec c2)
+
+	  | Fix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+	
+	  | CoFix(_,(_,types,terms)) -> 
+	       (try 
+		 iter_fail matchrec types
+	       with ex when catchable_exception ex -> 
+		 iter_fail matchrec terms)
+
+          | Prod (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | Lambda (_,t,c) ->
+	      (try 
+		 matchrec t 
+	       with ex when catchable_exception ex -> 
+		 matchrec c)
+          | _ -> error "Match_subterm")) 
+  in 
+  try matchrec cl
+  with ex when catchable_exception ex ->
+    raise (RefinerError (NoOccurrenceFound op))
+
+let unify_to_subterm_list allow_K clause oplist t = 
+  List.fold_right 
+    (fun op (clause,l) ->
+      if isMeta op then
+	if allow_K then (clause,op::l)
+	else error "Match_subterm"
+      else if occur_meta op then
+        let (clause',cl) =
+          try 
+	    (* This is up to delta for subterms w/o metas ... *)
+	    unify_to_subterm clause (strip_outer_cast op,t)
+          with RefinerError (NoOccurrenceFound _) when allow_K -> (clause,op)
+        in 
+	(clause',cl::l)
+      else if not allow_K & not (dependent op t) then
+	(* This is not up to delta ... *)
+	raise (RefinerError (NoOccurrenceFound op))
+      else
+	(clause,op::l))
+    oplist 
+    (clause,[])
+
+let secondOrderAbstraction allow_K typ (p, oplist) clause =
+  let env = w_env clause.hook in
+  let sigma = w_Underlying clause.hook in
+  let (clause',cllist) = unify_to_subterm_list allow_K clause oplist typ in
+  let typp = clenv_instance_type clause' p in 
+  let pred = abstract_list_all env sigma typp typ cllist in
+  clenv_unify_0 CONV (mkMeta p) pred clause'
+
+let clenv_unify2 allow_K cv_pb ty1 ty2 clause =
+  let c1, oplist1 = whd_stack ty1 in
+  let c2, oplist2 = whd_stack ty2 in
+  match kind_of_term c1, kind_of_term c2 with
+    | Meta p1, _ ->
+        (* Find the predicate *)
+	let clause' =
+          secondOrderAbstraction allow_K ty2 (p1,oplist1) clause in 
+        (* Resume first order unification *)
+	clenv_unify_0 cv_pb (clenv_instance_term clause' ty1) ty2 clause'
+    | _, Meta p2 ->
+        (* Find the predicate *)
+	let clause' =
+          secondOrderAbstraction allow_K ty1 (p2, oplist2) clause in 
+        (* Resume first order unification *)
+	clenv_unify_0 cv_pb ty1 (clenv_instance_term clause' ty2) clause'
+    | _ -> error "clenv_unify2"
+
+
+(* 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. *)
+
+(* 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_unify allow_K cv_pb ty1 ty2 clenv =
+  let hd1,l1 = whd_stack ty1 in
+  let hd2,l2 = whd_stack ty2 in
+  match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
+    (* Pattern case *)
+    | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
+      when List.length l1 = List.length l2 ->
+	(try 
+	   clenv_typed_unify cv_pb ty1 ty2 clenv
+	 with ex when catchable_exception ex -> 
+	   try 
+	     clenv_unify2 allow_K cv_pb ty1 ty2 clenv
+	   with RefinerError (NoOccurrenceFound c) as e -> raise e
+	     | ex when catchable_exception ex -> 
+	     error "Cannot solve a second-order unification problem")
+
+     (* Second order case *)
+     | (Meta _, true, _, _ | _, _, Meta _, true) -> 
+	(try 
+	   clenv_unify2 allow_K cv_pb ty1 ty2 clenv
+	with RefinerError (NoOccurrenceFound c) as e -> raise e
+	  | ex when catchable_exception ex -> 
+          try 
+	     clenv_typed_unify cv_pb ty1 ty2 clenv
+          with ex when catchable_exception ex -> 
+             error "Cannot solve a second-order unification problem")
+
+     (* General case: try first order *)
+     | _ -> clenv_unify_0 cv_pb ty1 ty2 clenv
+
+
+(* [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 metamap_in_dom mv ne then begin
+			    warning ("Cannot put metavar "^(string_of_meta mv)^
+				     " in name-environment twice");
+			    ne
+			  end else 
+			    Metamap.add mv id ne)
+          clenv.namenv (metamap_to_list subclenv.namenv);
+      env = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
+	       clenv.env (metamap_to_list subclenv.env);
+      hook = clenv.hook } 
+  in
+  (* unify the type of the template of [subclenv] with the type of [mv] *)
+  let clenv'' =
+    clenv_unify true CUMUL
+      (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
+
+(* [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 Metamap.find mv clenv.env with
+    | Clval(_,b) -> b.freemetas
+    | Cltyp b -> b.freemetas
+
+let clenv_template_metavars clenv = clenv.templval.freemetas
+
+(* [clenv_dependent hyps_only clenv]
+ * returns a list of the metavars which appear in the template of clenv,
+ * 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 the
+ * type of clenv.
+ * If [hyps_only] then metavariables occurring in the type are _excluded_ *)
+
+let dependent_metas clenv mvs conclmetas =
+  List.fold_right
+    (fun mv deps ->
+       Metaset.union deps (clenv_metavars clenv mv))
+    mvs conclmetas
+
+let clenv_dependent hyps_only clenv =
+  let mvs = collect_metas (clenv_instance_template clenv) in
+  let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  List.filter
+    (fun mv -> Metaset.mem mv deps && not (hyps_only && Metaset.mem mv ctyp_mvs))
+    mvs
+
+let clenv_missing c = clenv_dependent true c
+
+(* [clenv_independent clenv]
+ * 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 =
+  let mvs = collect_metas (clenv_instance_template clenv) in
+  let ctyp_mvs = metavars_of (clenv_instance_template_type clenv) in
+  let deps = dependent_metas clenv mvs ctyp_mvs in
+  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
+
+let w_coerce wc c ctyp target =
+  let j = make_judge c ctyp in
+  let env = w_env wc in
+  let isevars = Evarutil.create_evar_defs (w_Underlying wc) in
+  let j' = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
+  (* faire quelque chose avec isevars ? *)
+  j'.uj_val
+
+let clenv_constrain_dep_args hyps_only clause = function
+  | [] -> clause 
+  | mlist ->
+      let occlist = clenv_dependent hyps_only clause in
+      if List.length occlist = List.length mlist then
+	List.fold_left2
+          (fun clenv k c ->
+	    let wc = clause.hook in
+	    try
+	      let k_typ = w_hnf_constr wc (clenv_instance_type clause k) in
+	      let c_typ = w_hnf_constr wc (w_type_of wc c) in
+	      let c' = w_coerce wc c c_typ k_typ in
+	      clenv_unify true CONV (mkMeta k) c' clenv
+	    with _ ->
+              clenv_unify true CONV (mkMeta k) c clenv)
+          clause occlist mlist
+      else 
+	error ("Not the right number of missing arguments (expected "
+	       ^(string_of_int (List.length occlist))^")")
+
+let clenv_constrain_missing_args mlist clause =
+  clenv_constrain_dep_args true clause mlist
+
+let clenv_lookup_name clenv id =
+  match metamap_inv clenv.namenv id with
+    | []  -> 
+	errorlabstrm "clenv_lookup_name"
+          (str"No such bound variable " ++ pr_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 in 
+  let rec matchrec clause = function
+    | [] -> clause
+    | (loc,b,c)::t ->
+	let k =
+	  match b with
+            | NamedHyp s ->
+		if List.exists (fun (_,b',_) -> b=b') t then 
+		  errorlabstrm "clenv_match_args" 
+		    (str "The variable " ++ pr_id s ++ 
+		    str " occurs more than once in binding")
+		else
+		  clenv_lookup_name clause s
+	    | AnonHyp n ->
+		if List.exists (fun (_,b',_) -> b=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 _|Invalid_argument _) ->
+                  errorlabstrm "clenv_match_args" (str "No such binder")
+	in
+	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
+	(* nf_betaiota was before in type_of - useful to reduce types like *)
+	(* (x:A)([x]P u) *)
+	and c_typ = w_hnf_constr clause.hook
+          (nf_betaiota (w_type_of clause.hook c)) in
+	let cl =
+	  (* Try to infer some Meta/Evar from the type of [c] *)
+	  try 
+            clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
+	  with _ ->
+	  (* Try to coerce to the type of [k]; cannot merge with the
+	     previous case because Coercion does not handle Meta *)
+          let c' = w_coerce clause.hook c c_typ k_typ in
+	  try clenv_unify true CONV (mkMeta k) c' clause
+	  with RefinerError (CannotUnify (m,n)) ->
+	    Stdpp.raise_with_loc loc
+ 	      (RefinerError (CannotUnifyBindingType (m,n)))
+	in matchrec cl t
+  in 
+  matchrec clause s
+
+type arg_bindings = (int * constr) list
+
+let clenv_constrain_with_bindings bl clause =
+  if bl = [] then 
+    clause 
+  else 
+    let all_mvs = collect_metas (clenv_template clause).rebus in
+    let rec matchrec clause = function
+      | []       -> clause
+      | (n,c)::t ->
+          let k = 
+            (try
+              if n > 0 then 
+		List.nth all_mvs (n-1)
+              else if n < 0 then 
+		List.nth (List.rev all_mvs) (-n-1)
+              else error "clenv_constrain_with_bindings" 
+            with Failure _ ->
+              errorlabstrm "clenv_constrain_with_bindings"
+                (str"Clause did not have " ++ int n ++ str"-th" ++
+                str" absolute argument")) in
+	  let env = Global.env () in
+	  let sigma = Evd.empty in
+	  let k_typ = nf_betaiota (clenv_instance_type clause k) in
+	  let c_typ = nf_betaiota (w_type_of clause.hook c) in 
+	  matchrec
+            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
+    in 
+    matchrec clause bl
+
+
+(* [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 false clenv in
+  List.fold_left
+    (fun clenv mv ->
+       let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in
+       let (evar_n,_) = destEvar evar in
+       let tY = clenv_instance_type clenv mv in
+       let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in
+       clenv_assign mv evar clenv')
+    clenv
+    dep_mvs
+
+(***************************)
+
+let clenv_unique_resolver allow_K clause gl =
+  clenv_unify allow_K CUMUL
+    (clenv_instance_template_type clause) (pf_concl gl) clause 
+
+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 allow_K gls =
+  clenv_refine_cast kONT (clenv_unique_resolver allow_K clenv gls) gls
+
+let elim_res_pf_THEN_i kONT clenv tac gls =  
+  let clenv' = (clenv_unique_resolver true clenv gls) in
+  tclTHENLASTn (clenv_refine kONT clenv') (tac clenv') gls
+
+let e_res_pf kONT clenv gls =
+  clenv_refine kONT
+    (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+
+(* Clausal environment for an application *)
+
+let make_clenv_binding_gen n wc (c,t) = function
+  | ImplicitBindings largs ->
+      let clause = mk_clenv_from_n wc n (c,t) in
+      clenv_constrain_dep_args (n <> None) clause largs
+  | ExplicitBindings lbind ->
+      let clause = mk_clenv_rename_from_n wc n (c,t) in
+      clenv_match_args lbind clause
+  | NoBindings ->
+      mk_clenv_from_n wc n (c,t)
+
+let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
+let make_clenv_binding = make_clenv_binding_gen None
+
+open Printer
+
+let pr_clenv clenv =
+  let pr_name mv =
+    try 
+      let id = Metamap.find mv clenv.namenv in
+      (str"[" ++ pr_id id ++ str"]")
+    with Not_found -> (mt ())
+  in
+  let pr_meta_binding = function
+    | (mv,Cltyp b) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name mv ++ str " : " ++ prterm b.rebus ++ fnl ())
+    | (mv,Clval(b,_)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name mv ++ str " := " ++ prterm b.rebus ++ fnl ())
+  in
+  (str"TEMPL: " ++ prterm clenv.templval.rebus ++
+     str" : " ++ prterm clenv.templtyp.rebus ++ fnl () ++
+     (prlist pr_meta_binding (metamap_to_list clenv.env)))