deplacement de clenv vers pretyping

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

6 files changed, 693 insertions, 25 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
new file mode 100644
index 0000000000..0df34169a5
--- /dev/null
+++ b/pretyping/clenv.ml
@@ -0,0 +1,562 @@
+(************************************************************************)
+(*  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$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Environ
+open Evd
+open Reductionops
+open Rawterm
+open Pattern
+open Tacexpr
+open Tacred
+open Pretype_errors
+
+(* *)
+let get_env   evc = Global.env_of_context evc.it
+let w_type_of wc c  =
+  Typing.type_of (get_env wc) wc.sigma c
+let w_hnf_constr wc c        = hnf_constr (get_env wc) wc.sigma c
+let get_concl gl = gl.it.evar_concl
+
+(* 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)
+
+(* 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)
+
+(* Clausal environments *)
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Metamap.t;
+  env : meta_map;
+  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 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 gls clenv =
+  let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in
+  { clenv with hook = wc }
+
+let clenv_wtactic f clenv =
+  let (sigma',mmap') = f (clenv.hook.sigma, clenv.env) in
+  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=sigma'}}
+
+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 (get_env wc) [] t)
+
+let mk_clenv_rename_from_n wc n (c,t) = 
+  mk_clenv_from_n wc n (c,rename_bound_var (get_env wc) [] t)
+    
+let mk_clenv_rename_type_of wc t =
+  mk_clenv_from wc (t,rename_bound_var (get_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 (get_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)
+
+(* [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_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 (get_env ce.hook) ce.hook.sigma metamap c
+
+let clenv_instance_type_of ce c =
+  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+
+let clenv_unify allow_K cv_pb t1 t2 clenv =
+  let env = get_env clenv.hook in
+  clenv_wtactic (Unification.w_unify allow_K env cv_pb t1 t2) clenv
+
+let clenv_unique_resolver allow_K clause gl =
+  clenv_unify allow_K CUMUL
+    (clenv_instance_template_type clause) (get_concl gl) clause 
+
+(* [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'
+
+(* [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 = (mk_freelisted (clenv_instance_template_type clenv)).freemetas 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 = (mk_freelisted (clenv_instance_template_type clenv)).freemetas 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 = get_env wc in
+  let isevars = Evarutil.create_evar_defs wc.sigma 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 PretypeError (env,CannotUnify (m,n)) ->
+	    Stdpp.raise_with_loc loc
+ 	      (PretypeError (env,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
+
+
+(***************************)
+
+(* 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
+
+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 " : " ++ print_constr b.rebus ++ fnl ())
+    | (mv,Clval(b,_)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name mv ++ str " := " ++ print_constr b.rebus ++ fnl ())
+  in
+  (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
+     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
+     (prlist pr_meta_binding (metamap_to_list clenv.env)))
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
new file mode 100644
index 0000000000..ae5cafdf65
--- /dev/null
+++ b/pretyping/clenv.mli
@@ -0,0 +1,104 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*i*)
+open Util
+open Names
+open Term
+open Sign
+open Evd
+(*i*)
+
+(* [new_meta] is a generator of unique meta variables *)
+val new_meta : unit -> metavariable
+
+(* [exist_to_meta] generates new metavariables for each existential
+   and performs the replacement in the given constr *)
+val exist_to_meta :
+  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
+
+(* The Type of Constructions clausale environments. *)
+
+type 'a clausenv = {
+  templval : constr freelisted;
+  templtyp : constr freelisted;
+  namenv : identifier Metamap.t;
+  env : meta_map;
+  hook : 'a }
+
+type wc = named_context sigma (* for a better reading of the following *)
+
+(* [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. *)
+
+val collect_metas : constr -> metavariable list
+val mk_clenv : 'a -> constr -> 'a clausenv
+val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
+val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
+val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
+val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
+val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
+val mk_clenv_type_of : wc -> constr -> wc clausenv
+
+val subst_clenv : (substitution -> 'a -> 'a) -> 
+  substitution -> 'a clausenv -> 'a clausenv
+val clenv_wtactic :
+  (evar_map * meta_map -> evar_map * meta_map) -> wc clausenv -> wc clausenv
+
+val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
+val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
+val clenv_instance_term : wc clausenv -> constr -> constr
+val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
+val clenv_template : 'a clausenv -> constr freelisted
+val clenv_template_type : 'a clausenv -> constr freelisted
+val clenv_instance_type : wc clausenv -> metavariable -> constr
+val clenv_instance_template : wc clausenv -> constr
+val clenv_instance_template_type : wc clausenv -> constr
+val clenv_instance : 'a clausenv -> constr freelisted -> constr
+val clenv_type_of : wc clausenv -> constr -> constr
+val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+
+(* Unification with clenv *)
+type arg_bindings = (int * constr) list
+
+val clenv_unify : 
+  bool -> Reductionops.conv_pb -> constr -> constr ->
+  wc clausenv -> wc clausenv
+val clenv_match_args :
+  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
+val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+
+(* Bindings *)
+val clenv_independent : wc clausenv -> metavariable list
+val clenv_dependent : bool -> 'a clausenv -> metavariable list
+val clenv_missing : 'a clausenv -> metavariable list
+val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
+  constr list -> wc clausenv -> wc clausenv
+(*
+val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
+*)
+val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
+val clenv_unique_resolver :
+  bool -> wc clausenv -> evar_info sigma -> wc clausenv
+
+val make_clenv_binding_apply :
+  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
+val make_clenv_binding :
+  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
+
+(* Pretty-print *)
+val pr_clenv : 'a clausenv -> Pp.std_ppcmds
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index d7407c5d1d..84fd4798b7 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -27,6 +27,7 @@ type pretype_error =
   | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
   | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr
   (* Pretyping *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 2f9b1dc46a..fadd3f338f 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -29,6 +29,7 @@ type pretype_error =
   | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
   | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr
   (* Pretyping *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8c33a07465..359484997b 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -57,7 +57,7 @@ type maps = evar_map * meta_map
  * [c] is typed in the context of [sp] and evar context [evd] with
  * [sp] removed to avoid circular definitions.
  *)
-let w_Define evd sp c =
+let w_Define sp c evd =
   let sigma = evars_of evd in
   if Evd.is_defined sigma sp then
     error "Unify.w_Define: cannot define evar twice";
@@ -213,17 +213,17 @@ let is_mimick_head f =
       (Const _|Var _|Rel _|Construct _|Ind _) -> true
     | _ -> false
 
-let mimick_evar env evd hdc nargs sp =
+let mimick_evar env hdc nargs sp evd =
   let (sigma',c) = applyHead env (evars_of evd) nargs hdc in
   evars_reset_evd sigma' evd;
-  w_Define evd sp c
+  w_Define sp c evd
   
 
 (* [w_merge env sigma b metas evars] 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 w_merge env (sigma,metamap) with_types metas evars =
+let w_merge env with_types metas evars (sigma,metamap) =
   let evd = create_evar_defs sigma in
   let mmap = ref metamap in
   let ty_metas = ref [] in
@@ -254,14 +254,14 @@ let w_merge env (sigma,metamap) with_types metas evars =
                 match krhs with
 		  | App (f,cl) when is_mimick_head f ->
 		      (try 
-                        w_Define evd evn rhs'; 
+                        w_Define evn rhs' evd; 
 		        w_merge_rec metas t
 		      with ex when precatchable_exception ex ->
-                        mimick_evar env evd f (Array.length cl) evn;
+                        mimick_evar env f (Array.length cl) evn evd;
 			w_merge_rec metas evars)
                   | _ ->
                       (* ensure tail recursion in non-mimickable case! *)
-                      w_Define evd evn rhs'; 
+                      w_Define evn rhs' evd; 
 		      w_merge_rec metas t
 	      end
 
@@ -306,12 +306,12 @@ let w_merge env (sigma,metamap) with_types metas evars =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
-let w_unify_core_0 env evd with_types cv_pb m n =
+let w_unify_core_0 env with_types cv_pb m n evd =
   let (mc,ec) = unify_0 env (fst evd) cv_pb m n in 
-  w_merge env evd with_types mc ec
+  w_merge env with_types mc ec evd
 
-let w_unify_0 env evd = w_unify_core_0 env evd false
-let w_typed_unify env evd = w_unify_core_0 env evd true
+let w_unify_0 env = w_unify_core_0 env false
+let w_typed_unify env = w_unify_core_0 env true
 
 
 (* takes a substitution s, an open term op and a closed term cl
@@ -335,7 +335,7 @@ let w_unify_to_subterm env (op,cl) evd =
     let cl = strip_outer_cast cl in
     (try 
        if closed0 cl 
-       then w_unify_0 env evd CONV op cl,cl
+       then w_unify_0 env CONV op cl evd,cl
        else error "Bound 1"
      with ex when precatchable_exception ex ->
        (match kind_of_term cl with 
@@ -409,30 +409,30 @@ let w_unify_to_subterm_list env allow_K oplist t evd =
     oplist 
     (evd,[])
 
-let secondOrderAbstraction env evd allow_K typ (p, oplist) =
+let secondOrderAbstraction env allow_K typ (p, oplist) evd =
   let sigma = fst evd in
   let (evd',cllist) =
     w_unify_to_subterm_list env allow_K oplist typ evd in
   let typp = meta_type (snd evd') p in
   let pred = abstract_list_all env sigma typp typ cllist in
-  w_unify_0 env evd' CONV (mkMeta p) pred
+  w_unify_0 env CONV (mkMeta p) pred evd'
 
-let w_unify2 env evd allow_K cv_pb ty1 ty2 =
+let w_unify2 env allow_K cv_pb ty1 ty2 evd =
   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 evd' =
-          secondOrderAbstraction env evd allow_K ty2 (p1,oplist1) in 
+          secondOrderAbstraction env allow_K ty2 (p1,oplist1) evd in 
         (* Resume first order unification *)
-	w_unify_0 env evd' cv_pb (nf_meta (snd evd') ty1) ty2
+	w_unify_0 env cv_pb (nf_meta (snd evd') ty1) ty2 evd'
     | _, Meta p2 ->
         (* Find the predicate *)
 	let evd' =
-          secondOrderAbstraction env evd allow_K ty1 (p2, oplist2) in 
+          secondOrderAbstraction env allow_K ty1 (p2, oplist2) evd in 
         (* Resume first order unification *)
-	w_unify_0 env evd' cv_pb ty1 (nf_meta (snd evd') ty2)
+	w_unify_0 env cv_pb ty1 (nf_meta (snd evd') ty2) evd'
     | _ -> error "w_unify2"
 
 
@@ -464,10 +464,10 @@ let w_unify allow_K env cv_pb ty1 ty2 evd =
     | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
       when List.length l1 = List.length l2 ->
 	(try 
-	   w_typed_unify env evd cv_pb ty1 ty2
+	   w_typed_unify env cv_pb ty1 ty2 evd
 	 with ex when precatchable_exception ex -> 
 	   try 
-	     w_unify2 env evd allow_K cv_pb ty1 ty2
+	     w_unify2 env allow_K cv_pb ty1 ty2 evd
 	   with PretypeError (env,NoOccurrenceFound c) as e -> raise e
 	     | ex when precatchable_exception ex -> 
 	     error "Cannot solve a second-order unification problem")
@@ -475,14 +475,14 @@ let w_unify allow_K env cv_pb ty1 ty2 evd =
      (* Second order case *)
      | (Meta _, true, _, _ | _, _, Meta _, true) -> 
 	(try 
-	   w_unify2 env evd allow_K cv_pb ty1 ty2
+	   w_unify2 env allow_K cv_pb ty1 ty2 evd
 	with PretypeError (env,NoOccurrenceFound c) as e -> raise e
 	  | ex when precatchable_exception ex -> 
           try 
-	     w_typed_unify env evd cv_pb ty1 ty2
+	     w_typed_unify env cv_pb ty1 ty2 evd
           with ex when precatchable_exception ex -> 
              error "Cannot solve a second-order unification problem")
 
      (* General case: try first order *)
-     | _ -> w_unify_0 env evd cv_pb ty1 ty2
+     | _ -> w_unify_0 env cv_pb ty1 ty2 evd
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index ae276b2a82..d05b8cb5a8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -19,7 +19,7 @@ open Evd
 
 type maps = evar_map * meta_map
 
-val w_Define : Evarutil.evar_defs -> evar -> constr -> unit
+val w_Define : evar -> constr -> Evarutil.evar_defs -> unit
 
 (* The "unique" unification fonction *)
 val w_unify :