simplification de clenv

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

10 files changed, 254 insertions, 376 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index ef0425e37..45ead5a9f 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -27,17 +27,17 @@ open Evarutil
 open Unification
 
 (* *)
+let w_coerce wc c ctyp target =
+  let j = make_judge c ctyp in
+  let env = Global.env_of_context wc.it in
+  let isevars = create_evar_defs wc.sigma in
+  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
+  (evars_of evd',j'.uj_val)
+
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
 let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
-
-let get_env wc = Global.env_of_context wc.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
-
-let mk_wc gls = {it=gls.it.evar_hyps; sigma=gls.sigma}
+let pf_concl gl = gl.it.evar_concl
 
 (* Generator of metavariables *)
 let new_meta =
@@ -59,63 +59,45 @@ let exist_to_meta sigma (emap, c) =
       | _ -> 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 = {
+type wc = named_context sigma
+
+type clausenv = {
   templval : constr freelisted;
   templtyp : constr freelisted;
   namenv : identifier Metamap.t;
   env : meta_map;
-  hook : 'a }
+  hook : wc }
 
-type wc = named_context sigma
+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 clenv_nf_meta clenv c = nf_meta clenv.env c
 let clenv_meta_type clenv mv = meta_type clenv.env mv
 let clenv_value clenv = meta_instance clenv.env clenv.templval
 let clenv_type clenv = meta_instance clenv.env clenv.templtyp
 
-(* [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 cl_env ce = Global.env_of_context ce.hook.it
+
+let clenv_hnf_constr ce t = hnf_constr (cl_env ce) ce.hook.sigma t
+
+let clenv_get_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 (cl_env ce) ce.hook.sigma metamap c
+
 
-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
@@ -153,44 +135,39 @@ let mk_clenv_from_n gls n (c,cty) =
     templtyp = mk_freelisted concl;
     namenv = namenv;
     env = env;
-    hook = mk_wc gls }
+    hook = {it=gls.it.evar_hyps; sigma=gls.sigma} }
 
 let mk_clenv_from gls = mk_clenv_from_n gls 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 (evd',mmap') =
-    f (create_evar_defs clenv.hook.sigma, clenv.env) in
-  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
-
-let mk_clenv_hnf_constr_type_of gls t =
-  mk_clenv_from gls (t,pf_hnf_constr gls (pf_type_of gls t))
-
 let mk_clenv_rename_from gls (c,t) = 
   mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)
 
 let mk_clenv_rename_from_n gls n (c,t) = 
   mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
 
-let mk_clenv_rename_type_of gls t =
-  mk_clenv_from gls (t,rename_bound_var (pf_env gls) [] (pf_type_of gls t))
-    
-let mk_clenv_rename_hnf_constr_type_of gls t =
-  mk_clenv_from gls
-    (t,rename_bound_var (pf_env gls) [] (pf_hnf_constr gls (pf_type_of gls t)))
-
 let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
-			      
+
+(******************************************************************)
+
+(* [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
+
+let clenv_defined clenv mv = meta_defined clenv.env mv
+
+(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)		      
 let clenv_assign mv rhs clenv =
   let rhs_fls = mk_freelisted rhs in 
   if meta_exists (mentions clenv mv) rhs_fls.freemetas then
@@ -218,98 +195,94 @@ let clenv_assign mv rhs clenv =
   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_value0 clenv mv =
-  match Metamap.find mv clenv.env with
-    | Clval(b,_) -> b
-    | Cltyp _ -> failwith "clenv_value0"
-	  
-let clenv_type0 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_value0 clenv mv)
-    
-let clenv_instance_type clenv mv =
-  clenv_instance clenv (clenv_type0 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)
+let clenv_wtactic f clenv =
+  let (evd',mmap') =
+    f (create_evar_defs clenv.hook.sigma, clenv.env) in
+  {clenv with env = mmap' ; hook = {it=clenv.hook.it; sigma=evars_of evd'}}
+
+
+(* [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_ *)
+
+(* 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
-    Retyping.get_type_of_with_meta (get_env ce.hook) ce.hook.sigma metamap c
+  List.rev (collrec [] c)
+
+(* [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 = (meta_ftype clenv.env mv).freemetas
 
-let clenv_instance_type_of ce c =
-  clenv_instance ce (mk_freelisted (clenv_type_of ce c))
+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_value clenv) in
+  let ctyp_mvs = (mk_freelisted (clenv_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 ce = clenv_dependent true ce
+
+(******************************************************************)
 
 let clenv_unify allow_K cv_pb t1 t2 clenv =
-  let env = get_env clenv.hook in
+  let env = cl_env clenv in
   clenv_wtactic (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_unify allow_K CUMUL (clenv_type clause) (pf_concl gl) clause 
 
 
-(* [clenv_bchain mv clenv' clenv]
+(* [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 (cl_env clenv) in
+       let (evar_n,_) = destEvar evar in
+       let tY = clenv_meta_type clenv mv in
+       let clenv' =
+         clenv_wtactic (w_Declare (cl_env clenv) evar_n tY) clenv in
+       clenv_assign mv evar clenv')
+    clenv
+    dep_mvs
+
+let evar_clenv_unique_resolver clenv gls =
+  clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)
+
+
+(******************************************************************)
+
+let connect_clenv gls clenv =
+  let wc = {it=gls.it.evar_hyps; sigma=gls.sigma} in
+  { clenv with hook = wc }
+
+(* [clenv_fchain 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
@@ -319,15 +292,14 @@ let clenv_unique_resolver allow_K clause gl =
  * 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_fchain mv clenv nextclenv =
+  (* Add the metavars of [nextclenv] 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 
+			  if clenv_defined nextclenv mv then 
 			    ne
 			  else if metamap_in_dom mv ne then begin
 			    warning ("Cannot put metavar "^(string_of_meta mv)^
@@ -335,80 +307,28 @@ let clenv_bchain mv subclenv clenv =
 			    ne
 			  end else 
 			    Metamap.add mv id ne)
-          clenv.namenv (metamap_to_list subclenv.namenv);
+          clenv.namenv (metamap_to_list nextclenv.namenv);
       env = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
-	       clenv.env (metamap_to_list subclenv.env);
-      hook = clenv.hook } 
+	       clenv.env (metamap_to_list nextclenv.env);
+      hook = nextclenv.hook } 
   in
-  (* unify the type of the template of [subclenv] with the type of [mv] *)
+  (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
     clenv_unify true CUMUL
-      (clenv_instance clenv' (clenv_template_type subclenv))
-      (clenv_instance_type clenv' mv)
+      (clenv_nf_meta clenv' nextclenv.templtyp.rebus)
+      (clenv_meta_type clenv' mv)
       clenv' 
   in
   (* assign the metavar *)
   let clenv''' =
-    clenv_assign mv (clenv_instance clenv' (clenv_template subclenv)) clenv''
+    clenv_assign mv (clenv_nf_meta clenv' nextclenv.templval.rebus) clenv''
   in 
   clenv'''
 
+(***************************************************************)
+(* Bindings *)
 
-(* 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
+type arg_bindings = (int * constr) list
 
 (* [clenv_independent clenv]
  * returns a list of metavariables which appear in the term cval,
@@ -417,63 +337,11 @@ let clenv_missing c = clenv_dependent true c
  * 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 mvs = collect_metas (clenv_value clenv) in
+  let ctyp_mvs = (mk_freelisted (clenv_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 = create_evar_defs wc.sigma in
-  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env isevars j target in
-  (evars_of evd',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
-              (* faire quelque chose avec le sigma retourne ? *)
-	      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))^")")
-
-(* [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 (get_env clenv.hook) in
-       let (evar_n,_) = destEvar evar in
-       let tY = clenv_instance_type clenv mv in
-       let clenv' =
-         clenv_wtactic (w_Declare (get_env clenv.hook) evar_n tY) clenv in
-       clenv_assign mv evar clenv')
-    clenv
-    dep_mvs
-
-let evar_clenv_unique_resolver clenv gls =
-  clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)
-
-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
     | []  -> 
@@ -484,6 +352,8 @@ let clenv_lookup_name clenv id =
     |  _  -> 
 	 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
@@ -508,11 +378,11 @@ let clenv_match_args s clause =
 		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)
+	let k_typ = clenv_hnf_constr clause (clenv_meta_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
+	and c_typ =
+          clenv_hnf_constr clause (nf_betaiota (clenv_get_type_of clause c)) in
 	let cl =
 	  (* Try to infer some Meta/Evar from the type of [c] *)
 	  try 
@@ -529,13 +399,12 @@ let clenv_match_args s clause =
   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 all_mvs = collect_metas clause.templval.rebus in
     let rec matchrec clause = function
       | []       -> clause
       | (n,c)::t ->
@@ -550,16 +419,42 @@ let clenv_constrain_with_bindings bl clause =
               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 
+	  let k_typ = nf_betaiota (clenv_meta_type clause k) in
+	  let c_typ = nf_betaiota (clenv_get_type_of clause c) in 
 	  matchrec
             (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
     in 
     matchrec clause bl
 
 
+(* not exported: maybe useful ? *)
+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 =
+                clenv_hnf_constr clause (clenv_meta_type clause k) in
+	      let c_typ =
+                clenv_hnf_constr clause (clenv_get_type_of clause c) in
+              (* faire quelque chose avec le sigma retourne ? *)
+	      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
+
+
 (***************************)
 
 (* Clausal environment for an application *)
@@ -580,8 +475,7 @@ let make_clenv_binding = make_clenv_binding_gen None
 
 
 
-
-
+(****************************************************************)
 
 let pr_clenv clenv =
   let pr_name mv =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9ed07fc0d..375d84eac 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -34,38 +34,42 @@ val exist_to_meta :
  *          use in instanciating metavars by name.
  * [evd] is the mapping from metavar and evar numbers to their types
  *       and values.
- * [hook] is generally signature (named_context) and a sigma: the
+ * [hook] is a signature (named_context) and a sigma: the
  *        typing context
  *)
-type 'a clausenv = {
+type wc = named_context sigma (* for a better reading of the following *)
+type 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 *)
+  hook : wc }
 
-val subst_clenv : (substitution -> 'a -> 'a) -> 
-  substitution -> 'a clausenv -> 'a clausenv
+val subst_clenv :
+  (substitution -> wc -> wc) -> substitution -> clausenv -> clausenv
 
-val clenv_nf_meta   : wc clausenv -> constr -> constr
-val clenv_meta_type : wc clausenv -> int -> constr
-val clenv_value     : wc clausenv -> constr
-val clenv_type      : wc clausenv -> constr
+(* subject of clenv (instantiated) *)
+val clenv_value     : clausenv -> constr
+(* type of clanv (instantiated) *)
+val clenv_type      : clausenv -> types
+(* substitute resolved metas *)
+val clenv_nf_meta   : clausenv -> constr -> constr
+(* type of a meta in clenvś context *)
+val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : evar_info sigma -> constr * constr -> wc clausenv
+val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_from_n :
-  evar_info sigma -> int option -> constr * constr -> wc clausenv
+  evar_info sigma -> int option -> constr * types -> clausenv
+val mk_clenv_rename_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_rename_from_n :
-  evar_info sigma -> int option -> constr * constr -> wc clausenv
-val mk_clenv_type_of : evar_info sigma -> constr -> wc clausenv
+  evar_info sigma -> int option -> constr * types -> clausenv
+val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
 
 (***************************************************************)
 (* linking of clenvs *)
 
-val connect_clenv : evar_info sigma -> 'a clausenv -> wc clausenv
-val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
+val connect_clenv : evar_info sigma -> clausenv -> clausenv
+val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv
 
 (***************************************************************)
 (* Unification with clenvs *)
@@ -73,16 +77,16 @@ val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
 (* Unifies two terms in a clenv. The boolean is allow_K (see Unification) *)
 val clenv_unify : 
   bool -> Reductionops.conv_pb -> constr -> constr ->
-  wc clausenv -> wc clausenv
+  clausenv -> clausenv
 
 (* unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
-  bool -> wc clausenv -> evar_info sigma -> wc clausenv
+  bool -> clausenv -> evar_info sigma -> clausenv
 
 (* same as above (allow_K=false) but replaces remaining metas
    with fresh evars *)
 val evar_clenv_unique_resolver :
-  wc clausenv -> evar_info sigma -> wc clausenv
+  clausenv -> evar_info sigma -> clausenv
 
 (***************************************************************)
 (* Bindings *)
@@ -92,51 +96,31 @@ val evar_clenv_unique_resolver :
    start from the rightmost argument of the template. *)
 type arg_bindings = (int * constr) list
 
-val clenv_independent : wc clausenv -> metavariable list
-val clenv_missing : 'a clausenv -> metavariable list
-val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
+val clenv_independent : clausenv -> metavariable list
+val clenv_missing : clausenv -> metavariable list
+val clenv_lookup_name : clausenv -> identifier -> metavariable
 
 (* defines metas corresponding to the name of the bindings *)
 val clenv_match_args :
-  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
+  constr Rawterm.explicit_bindings -> clausenv -> clausenv
+val clenv_constrain_with_bindings : arg_bindings -> clausenv -> clausenv
 
 (* start with a clenv to refine with a given term with bindings *)
 
 (* 1- the arity of the lemma is fixed *)
 val make_clenv_binding_apply :
   evar_info sigma -> int -> constr * constr -> constr Rawterm.bindings ->
-   wc clausenv
+   clausenv
 val make_clenv_binding :
-  evar_info sigma -> constr * constr -> constr Rawterm.bindings -> wc clausenv
+  evar_info sigma -> constr * constr -> constr Rawterm.bindings -> clausenv
 
 (***************************************************************)
 (* Pretty-print *)
-val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+val pr_clenv : clausenv -> Pp.std_ppcmds
 
 (***************************************************************)
 (* Old or unused stuff... *)
 
-val collect_metas : constr -> metavariable list
-val mk_clenv : 'a -> constr -> 'a clausenv
-
-val mk_clenv_rename_from : evar_info sigma -> constr * constr -> wc clausenv
-val mk_clenv_hnf_constr_type_of : evar_info sigma -> constr -> wc clausenv
-
 val clenv_wtactic :
-  (evar_defs * meta_map -> evar_defs * meta_map) -> wc 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_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_dependent : bool -> 'a clausenv -> metavariable list
-val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
-  constr list -> wc clausenv -> wc clausenv
+  (evar_defs * meta_map -> evar_defs * meta_map) -> clausenv -> clausenv
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index bc50fdd2a..2d972068d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -50,7 +50,7 @@ let clenv_cast_meta clenv =
 	  (try 
 	     match Metamap.find mv clenv.env with
                | Cltyp b ->
-		   let b' = clenv_instance clenv b in 
+		   let b' = clenv_nf_meta clenv b.rebus in 
 		   if occur_meta b' then u else mkCast (mkMeta mv, b')
 	       | Clval(_) -> u
 	   with Not_found -> 
@@ -66,12 +66,12 @@ let clenv_cast_meta clenv =
 let clenv_refine clenv gls =
   tclTHEN
     (tclEVARS clenv.hook.sigma) 
-    (refine (clenv_instance_template clenv)) gls
+    (refine (clenv_value clenv)) gls
 
 let clenv_refine_cast clenv gls =
   tclTHEN
     (tclEVARS clenv.hook.sigma) 
-    (refine (clenv_cast_meta clenv (clenv_instance_template clenv)))
+    (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
 let res_pf clenv gls =
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 1695db2f5..c463d75e3 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -20,9 +20,9 @@ open Proof_type
 
 (* Tactics *)
 val unify : constr -> tactic
-val clenv_refine : wc clausenv -> tactic
-val res_pf      : wc clausenv -> tactic
-val res_pf_cast : wc clausenv -> tactic
-val elim_res_pf : wc clausenv -> bool -> tactic
-val e_res_pf : wc clausenv -> tactic
-val elim_res_pf_THEN_i : wc clausenv -> (wc clausenv -> tactic array) -> tactic
+val clenv_refine : clausenv -> tactic
+val res_pf      : clausenv -> tactic
+val res_pf_cast : clausenv -> tactic
+val elim_res_pf : clausenv -> bool -> tactic
+val e_res_pf : clausenv -> tactic
+val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0dc0a9f4c..66454059e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -44,10 +44,10 @@ open Tacexpr
 (****************************************************************************)
 
 type auto_tactic = 
-  | Res_pf     of constr * wc clausenv (* Hint Apply *)
-  | ERes_pf    of constr * wc clausenv (* Hint EApply *)
+  | Res_pf     of constr * clausenv (* Hint Apply *)
+  | ERes_pf    of constr * clausenv (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
   | Unfold_nth of global_reference       (* Hint Unfold *)
   | Extern     of glob_tactic_expr       (* Hint Extern *) 
 
@@ -195,7 +195,7 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
   match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = (clenv_template_type ce).rebus in
+	let c' = clenv_type ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
                   with BoundPattern -> failwith "make_apply_entry") in
@@ -263,7 +263,7 @@ let make_trivial env sigma (name,c) =
   let ce = mk_clenv_from dummy_goal (c,t) in
   (hd, { hname = name;
 	       pri=1;
-               pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus);
+               pat = Some (Pattern.pattern_of_constr (clenv_type ce));
                code=Res_pf_THEN_trivial_fail(c,ce) })
 
 open Vernacexpr
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 18daa6ebe..950e272bc 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ open Vernacexpr
 (*i*)
   
 type auto_tactic = 
-  | Res_pf     of constr * wc clausenv    (* Hint Apply *)
-  | ERes_pf    of constr * wc clausenv    (* Hint EApply *)
+  | Res_pf     of constr * clausenv    (* Hint Apply *)
+  | ERes_pf    of constr * clausenv    (* Hint EApply *)
   | Give_exact of constr                  
-  | Res_pf_THEN_trivial_fail of constr * wc clausenv (* Hint Immediate *)
+  | Res_pf_THEN_trivial_fail of constr * clausenv (* Hint Immediate *)
   | Unfold_nth of global_reference          (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr   (* Hint Extern *)
 
@@ -139,7 +139,7 @@ val priority : (int * 'a) list -> 'a list
 val default_search_depth : int ref
 
 (* Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : (constr * wc clausenv) -> tactic
+val unify_resolve : (constr * clausenv) -> tactic
 
 (* [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9a02ba608..0ac120327 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -448,8 +448,8 @@ let raw_inversion inv_kind indbinding id status names gl =
   let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in
   let indclause = mk_clenv_from gl (c,t) in
   let indclause' = clenv_constrain_with_bindings indbinding indclause in
-  let newc = clenv_instance_template indclause' in
-  let ccl = clenv_instance_template_type indclause' in
+  let newc = clenv_value indclause' in
+  let ccl = clenv_type indclause' in
   check_no_metas indclause' ccl;
   let IndType (indf,realargs) =
     try find_rectype env sigma ccl
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 7961a7dc9..905ca60b4 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -961,9 +961,9 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
      Clenv.clenv_wtactic
        (fun evd-> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd))
        cl in
-   let c1 = Clenv.clenv_instance_term cl' c1 in
-   let c2 = Clenv.clenv_instance_term cl' c2 in
-   (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2
+   let c1 = Clenv.clenv_nf_meta cl' c1 in
+   let c2 = Clenv.clenv_nf_meta cl' c2 in
+   (lft2rgt,Clenv.clenv_value cl'), c1, c2
  in
   let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in
   let marked_but = mark_occur c1 but in
@@ -979,8 +979,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl =
 let general_s_rewrite lft2rgt c gl =
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) =
-  decompose_app (Clenv.clenv_instance_template_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
  let rec get_last_two = function
    | [c1;c2] -> (c1, c2)
    | x::y::z -> get_last_two (y::z)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fa5eeaef3..79aa71c0f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -359,8 +359,8 @@ let general_elim_then_using
                    0 branchsigns.(i);
                branchnum = i+1;
                ity = ity;
-               largs = List.map (clenv_instance_term ce) largs;
-               pred = clenv_instance_term ce hd }
+               largs = List.map (clenv_nf_meta ce) largs;
+               pred = clenv_nf_meta ce hd }
     in 
     tac ba gl
   in
@@ -368,7 +368,8 @@ let general_elim_then_using
   let elimclause' =
     match predicate with
        | None   -> elimclause'
-       | Some p -> clenv_assign pmv p elimclause'
+       | Some p ->
+           clenv_unify true Reductionops.CONV (mkMeta pmv) p elimclause'
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d64c90916..57804f23a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -830,7 +830,7 @@ let rec intros_clearing = function
 
 let new_hyp mopt (c,lbind) g =
   let clause  = make_clenv_binding g (c,pf_type_of g c) lbind in
-  let (thd,tstack) = whd_stack (clenv_instance_template clause) in
+  let (thd,tstack) = whd_stack (clenv_value clause) in
   let nargs = List.length tstack in
   let cut_pf = 
     applist(thd, 
@@ -899,7 +899,7 @@ let last_arg c = match kind_of_term c with
 	
 let elimination_clause_scheme elimclause indclause allow_K gl = 
   let indmv = 
-    (match kind_of_term (last_arg (clenv_template elimclause).rebus) with
+    (match kind_of_term (last_arg elimclause.templval.rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              (str "The type of elimination clause is not well-formed")) 
@@ -911,7 +911,7 @@ let elimination_clause_scheme elimclause indclause allow_K gl =
  * refine fails *)
 
 let type_clenv_binding wc (c,t) lbind = 
-  clenv_instance_template_type (make_clenv_binding wc (c,t) lbind)
+  clenv_type (make_clenv_binding wc (c,t) lbind)
 
 (* 
  * Elimination tactic with bindings and using an arbitrary 
@@ -976,12 +976,12 @@ let elimination_in_clause_scheme id elimclause indclause gl =
           (str "The type of elimination clause is not well-formed") in
   let elimclause'  = clenv_fchain indmv elimclause indclause in 
   let hyp = mkVar id in
-  let hyp_typ = clenv_type_of elimclause' hyp in
+  let hyp_typ = pf_type_of gl hyp in
   let hypclause =
     mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
-  let new_hyp_prf  = clenv_instance_template elimclause'' in
-  let new_hyp_typ  = clenv_instance_template_type elimclause'' in
+  let new_hyp_prf  = clenv_value elimclause'' in
+  let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in" 
       (str "Nothing to rewrite in " ++ pr_id id);
@@ -1662,11 +1662,11 @@ let simple_destruct = function
 
 let elim_scheme_type elim t gl =
   let clause = mk_clenv_type_of gl elim in
-  match kind_of_term (last_arg (clenv_template clause).rebus) with
+  match kind_of_term (last_arg clause.templval.rebus) with
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify true CUMUL t (clenv_instance_type clause mv) clause in
+	  clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in
 	elim_res_pf clause' true gl
     | _ -> anomaly "elim_scheme_type"