restructuration des printers: proofs passe avant parsing

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

15 files changed, 438 insertions, 335 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 9e10c93909..146861a1cb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1699,21 +1699,23 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
   | (Some pred,x) ->
       let loc = loc_of_rawconstr pred in
       let dep, n, predj =
-	let isevars_copy = Evd.evars_of !isevars in
+	let isevars_copy = !isevars in
         (* We first assume the predicate is non dependent *)
 	let ndep_arity = build_expected_arity env isevars false tomatchs in
         try
 	  false, nb_prod ndep_arity, typing_fun (mk_tycon ndep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	    Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        isevars := Evd.evars_reset_evd isevars_copy !isevars;
+        (* Backtrack! *)
+        isevars := isevars_copy;
         (* We then assume the predicate is dependent *)
 	let dep_arity = build_expected_arity env isevars true tomatchs in
 	try
 	  true, nb_prod dep_arity, typing_fun (mk_tycon dep_arity) env pred
 	with PretypeError _ | TypeError _ |
 	  Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) ->
-        isevars := Evd.evars_reset_evd isevars_copy !isevars;
+        (* Backtrack again! *)
+        isevars := isevars_copy;
         (* Otherwise we attempt to type it without constraints, possibly *)
         (* failing with an error message; it may also be well-typed *)
 	(* but fails to satisfy arity constraints in case_dependent *)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 450c87a1f0..35de784e78 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -44,8 +44,7 @@ type clausenv = {
   templenv : env;
   env      : evar_defs;
   templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv   : identifier Metamap.t }
+  templtyp : constr freelisted }
 
 let cl_env ce = ce.templenv
 let cl_sigma ce = evars_of ce.env
@@ -53,15 +52,11 @@ let cl_sigma ce = evars_of ce.env
 let subst_clenv sub clenv = 
   { templval = map_fl (subst_mps sub) clenv.templval;
     templtyp = map_fl (subst_mps sub) clenv.templtyp;
-    namenv = clenv.namenv;
-    env = reset_evd
-      (evars_of clenv.env,
-       Metamap.map (map_clb (subst_mps sub)) (metas_of clenv.env))
-      clenv.env;
+    env = subst_evar_defs sub clenv.env;
     templenv = clenv.templenv }
 
 let clenv_nf_meta clenv c = nf_meta clenv.env c
-let clenv_meta_type clenv mv = meta_type clenv.env mv
+let clenv_meta_type clenv mv = Typing.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
 
@@ -72,50 +67,34 @@ 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 (metas_of ce.env)) in
+	 | (n,Clval(_,_,typ)) -> (n,typ.rebus)
+         | (n,Cltyp (_,typ))    -> (n,typ.rebus))
+      (meta_list ce.env) in
   Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c
 
-
-
 let clenv_environments evd bound c =
-  let rec clrec (ne,e,metas) n c =
+  let rec clrec (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
+      | (Some 0, _) -> (e, List.rev metas, c)
+      | (n, Cast (c,_)) -> clrec (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' = meta_declare mv c1 e in
-	  clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+	  let na' = if dep then na else Anonymous in
+	  let e' = meta_declare mv c1 ~name:na' e in
+	  clrec (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)
+	  clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+      | (n, _) -> (e, List.rev metas, c)
   in 
-  clrec (Metamap.empty,evd,[]) bound c
+  clrec (evd,[]) bound c
 
 let mk_clenv_from_n gls n (c,cty) =
   let evd = create_evar_defs gls.sigma in
-  let (namenv,env,args,concl) = clenv_environments evd n cty in
+  let (env,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
-    namenv = namenv;
     env = env;
     templenv = Global.env_of_context gls.it.evar_hyps }
 
@@ -135,41 +114,41 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
  * mv0, or if one of the free vars on mv1's freelist mentions
  * mv0 *)
 
-let mentions clenv mv0 = 
+let mentions clenv mv0 =
   let rec menrec mv1 =
-    try
-     (match Metamap.find mv1 (metas_of clenv.env) with
-	 | Clval (b,_) -> 
-	     Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas
-	 | Cltyp _ -> false)
-    with Not_found -> 
-      false
-  in 
-  menrec
+    mv0 = mv1 ||
+    let mlist =
+      try (meta_fvalue clenv.env mv1).freemetas
+      with Anomaly _ | Not_found -> Metaset.empty in
+    meta_exists menrec mlist
+  in menrec
 
 let clenv_defined clenv mv = meta_defined clenv.env mv
 
+let error_incompatible_inst clenv mv  =
+  let na = meta_name clenv.env mv in
+  match na with
+      Name id ->
+        errorlabstrm "clenv_assign"
+          (str "An incompatible instantiation has already been found for " ++ 
+           pr_id id)
+    | _ ->
+        anomaly "clenv_assign: non dependent metavar already assigned"
+
 (* 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
-    error "clenv__assign: circularity in unification";
+    error "clenv_assign: circularity in unification";
   try
-    (match Metamap.find mv (metas_of clenv.env) with
-       | Clval (fls,ty) ->
-	   if not (eq_constr fls.rebus rhs) then
-	     try 
-	       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 _ -> {clenv with env = meta_assign mv rhs_fls.rebus clenv.env})
+    if meta_defined clenv.env mv then
+      if not (eq_constr (meta_fvalue clenv.env mv).rebus rhs) then
+        error_incompatible_inst clenv mv
+      else
+	clenv
+    else {clenv with env = meta_assign mv rhs_fls.rebus clenv.env}
   with Not_found -> 
-    error "clenv_assign"
+    error "clenv_assign: undefined meta"
 
 
 let clenv_wtactic f clenv = {clenv with env = f clenv.env }
@@ -267,27 +246,14 @@ let clenv_fchain mv clenv nextclenv =
   let clenv' =
     { templval = clenv.templval;
       templtyp = clenv.templtyp;
-      namenv =
-	List.fold_left (fun ne (mv,id) ->
-			  if clenv_defined nextclenv 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 nextclenv.namenv);
       env = meta_merge clenv.env nextclenv.env;
-      templenv = nextclenv.templenv } 
-  in
+      templenv = nextclenv.templenv } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
     clenv_unify true CUMUL
       (clenv_nf_meta clenv' nextclenv.templtyp.rebus)
       (clenv_meta_type clenv' mv)
-      clenv' 
-  in
+      clenv' in
   (* assign the metavar *)
   let clenv''' =
     clenv_assign mv (clenv_nf_meta clenv' nextclenv.templval.rebus) clenv''
@@ -311,42 +277,29 @@ let clenv_independent clenv =
   let deps = dependent_metas clenv mvs ctyp_mvs in
   List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
 
-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 meta_of_binder clause loc b t mvs =
+  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");
+	meta_with_name clause.env 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")
 
 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 = meta_of_binder clause loc b t mvs in
 	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) *)
@@ -354,9 +307,8 @@ let clenv_match_args s clause =
           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 
-            clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
-	  with _ ->
+	  try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)
+	  with e when precatchable_exception e ->
 	  (* Try to coerce to the type of [k]; cannot merge with the
 	     previous case because Coercion does not handle Meta *)
             let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in
@@ -423,8 +375,7 @@ let clenv_constrain_missing_args mlist clause =
   clenv_constrain_dep_args true clause mlist
 
 
-(***************************)
-
+(****************************************************************)
 (* Clausal environment for an application *)
 
 let make_clenv_binding_gen n gls (c,t) = function
@@ -440,26 +391,11 @@ let make_clenv_binding_gen n gls (c,t) = function
 let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
 let make_clenv_binding = make_clenv_binding_gen None
 
-
-
-
 (****************************************************************)
+(* Pretty-print *)
 
 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 ++
+  h 0
+    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
      str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
-     (prlist pr_meta_binding (metamap_to_list (metas_of clenv.env))))
+     pr_evar_defs clenv.env)
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index cb53feb908..0c19a60f98 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -33,15 +33,16 @@ type clausenv = {
   templenv : env;
   env      : evar_defs;
   templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv   : identifier Metamap.t }
+  templtyp : constr freelisted }
 
-(* Substitution is not applied neither to the evar_map of evar_defs nor hook *)
+(* Substitution is not applied on templenv (because subst_clenv is
+   applied only on hints which typing env is overwritten by the
+   goal env) *)
 val subst_clenv : substitution -> clausenv -> clausenv
 
 (* subject of clenv (instantiated) *)
 val clenv_value     : clausenv -> constr
-(* type of clanv (instantiated) *)
+(* type of clenv (instantiated) *)
 val clenv_type      : clausenv -> types
 (* substitute resolved metas *)
 val clenv_nf_meta   : clausenv -> constr -> constr
@@ -88,7 +89,6 @@ type arg_bindings = (int * constr) list
 
 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 :
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 276c455fe1..52a8997144 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -19,7 +19,6 @@ open Sign
 open Environ
 open Evd
 open Reductionops
-open Indrec
 open Pretype_errors
 
 
@@ -120,16 +119,14 @@ let exist_to_meta sigma (emap, c) =
 (*************************************)
 (* Metas *)
 
-let meta_val_of evd mv = 
-  let env = metas_of evd in
+let meta_value evd mv = 
   let rec valrec mv =
     try
-      (match Metamap.find mv env with
-	 | Cltyp _ -> mkMeta mv
-	 | Clval(b,_) ->
-	     instance (List.map (fun mv' -> (mv',valrec mv')) 
-			       (Metaset.elements b.freemetas)) b.rebus)
-    with Not_found -> 
+      let b = meta_fvalue evd mv in
+      instance
+        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+        b.rebus
+    with Anomaly _ | Not_found -> 
       mkMeta mv
   in 
   valrec mv
@@ -137,7 +134,7 @@ let meta_val_of evd mv =
 let meta_instance env b =
   let c_sigma =
     List.map 
-      (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas)
+      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
   in 
   instance c_sigma b.rebus
 
@@ -231,20 +228,13 @@ let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
   evd := evd';
   ev
 
-(* We don't try to guess in which sort the type should be defined, since
-   any type has type Type. May cause some trouble, but not so far... *)
-
-let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
-(*
-let new_Type () = mkType dummy_univ
-
-let new_Type_sort () = Type dummy_univ
-
-let judge_of_new_Type () = 
-  { uj_val = mkSort (Type dummy_univ);
-    uj_type = mkSort (Type dummy_univ) }
-*)
-
+(* declare a new evar (tactic style) *)
+let w_Declare env sp ty evd =
+  let sigma = evars_of evd in
+  if Evd.in_dom sigma sp then
+    error "w_Declare: cannot redeclare evar";
+  let _ = Typing.type_of env sigma ty in (* Checks there is no meta *)
+  Evd.evar_declare (named_context env) sp ty evd
 
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -348,7 +338,7 @@ let real_clean env isevars ev args rhs =
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
 
-let evar_define env isevars (ev,argsv) rhs =
+let evar_define env (ev,argsv) rhs isevars =
   if occur_evar ev rhs
   then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
@@ -359,6 +349,35 @@ let evar_define env isevars (ev,argsv) rhs =
   let isevars'' = Evd.evar_define ev body isevars' in
   isevars'',[ev]
 
+(* [w_Define evd sp c] (tactic style)
+ *
+ * Defines evar [sp] with term [c] in evar context [evd].
+ * [c] is typed in the context of [sp] and evar context [evd] with
+ * [sp] removed to avoid circular definitions.
+ * No unification is performed in order to assert that [c] has the
+ * correct type.
+ *)
+let w_Define sp c evd =
+  let sigma = evars_of evd in
+  if not (Evd.in_dom sigma sp) then
+    error "w_Define: cannot define undeclared evar";
+  if Evd.is_defined sigma sp then
+    error "w_Define: cannot define evar twice";
+  let spdecl = Evd.map sigma sp in
+  let env = evar_env spdecl in
+  let _ =
+    (* Do not consider the metamap because evars may not depend on metas *)
+    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
+    with
+	Not_found -> error "Instantiation contains unlegal variables"
+      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
+      errorlabstrm "w_Define"
+      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
+       str (string_of_existential sp)) in
+  let spdecl' = { spdecl with evar_body = Evar_defined c } in
+  evars_reset_evd (Evd.add sigma sp spdecl') evd
+
+
 (*-------------------*)
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
@@ -468,11 +487,11 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  solve_refl conv_algo env isevars n1 args1 args2
 	else
 	  if Array.length args1 < Array.length args2 then 
-	    evar_define env isevars ev2 (mkEvar ev1)
+	    evar_define env ev2 (mkEvar ev1) isevars
 	  else 
-	    evar_define env isevars ev1 t2
+	    evar_define env ev1 t2 isevars
     | _ ->
-	evar_define env isevars ev1 t2 in
+	evar_define env ev1 t2 isevars in
   let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
   List.fold_left
     (fun (isevars,b as p) (pbty,t1,t2) ->
@@ -537,6 +556,11 @@ let define_evar_as_sort isevars (ev,args) =
   Evd.evar_define ev s isevars, destSort s
 
 
+(* We don't try to guess in which sort the type should be defined, since
+   any type has type Type. May cause some trouble, but not so far... *)
+
+let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
+
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
    constraint on its domain and codomain. If the input constraint is
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 711e107079..d62948b56e 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -21,42 +21,14 @@ open Reductionops
 
 (*s This modules provides useful functions for unification modulo evars *)
 
-(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
-(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
-
-val nf_evar :  evar_map -> constr -> constr
-val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar :
-   evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar :
-   evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar :
-   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
-val nf_evar_info : evar_map -> evar_info -> evar_info
-
-(* Replacing all evars *)
-exception Uninstantiated_evar of existential_key
-val whd_ise :  evar_map -> constr -> constr
-val whd_castappevar :  evar_map -> constr -> constr
-
 (***********************************************************)
 (* Metas *)
 
 (* [new_meta] is a generator of unique meta variables *)
 val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
-val nf_meta       : evar_defs -> constr -> constr
-val meta_type     : evar_defs -> metavariable -> types
-val meta_instance : evar_defs -> constr freelisted -> constr
-
-(* [exist_to_meta] generates new metavariables for each existential
-   and performs the replacement in the given constr *)
-val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr)
-
 
 (***********************************************************)
-
 (* Creating a fresh evar given their type and context *)
 val new_evar :
   evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr
@@ -78,10 +50,30 @@ val new_evar_instance :
    same as the evar context *)
 val make_evar_instance : env -> constr list
 
+val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
+
 (***********************************************************)
+(* Instanciate evars *)
+
+val w_Define : evar -> constr -> evar_defs -> evar_defs
+
+(* suspicious env ? *)
+val evar_define :
+  env -> existential -> constr -> evar_defs -> evar_defs * evar list
+
+
+(***********************************************************)
+(* Evars/Metas switching... *)
+
+(* [exist_to_meta] generates new metavariables for each existential
+   and performs the replacement in the given constr *)
+val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr)
 
 val non_instantiated : evar_map -> (evar * evar_info) list
 
+(***********************************************************)
+(* Unification utils *)
+
 val has_undefined_evars :  evar_defs -> constr -> bool
 val is_eliminator : constr -> bool
 val head_is_embedded_evar :  evar_defs -> constr -> bool
@@ -114,3 +106,23 @@ val valcon_of_tycon : type_constraint -> val_constraint
 
 val lift_tycon : type_constraint -> type_constraint
 
+(***********************************************************)
+
+(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
+(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
+
+val nf_evar :  evar_map -> constr -> constr
+val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
+val jl_nf_evar :
+   evar_map -> unsafe_judgment list -> unsafe_judgment list
+val jv_nf_evar :
+   evar_map -> unsafe_judgment array -> unsafe_judgment array
+val tj_nf_evar :
+   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+
+val nf_evar_info : evar_map -> evar_info -> evar_info
+
+(* Replacing all evars *)
+exception Uninstantiated_evar of existential_key
+val whd_ise :  evar_map -> constr -> constr
+val whd_castappevar :  evar_map -> constr -> constr
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c91d9ae7da..9799989870 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -8,9 +8,12 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
+open Nameops
 open Term
+open Termops
 open Sign
 open Environ
 open Libnames
@@ -155,37 +158,35 @@ let metavars_of c =
 let mk_freelisted c =
   { rebus = c; freemetas = metavars_of c }
 
+let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+
 
 (* Clausal environments *)
 
 type clbinding =
-  | Cltyp of constr freelisted
-  | Clval of constr freelisted * constr freelisted
-
-let map_fl f cfl = { cfl with rebus=f cfl.rebus }
+  | Cltyp of name * constr freelisted
+  | Clval of name * constr freelisted * constr freelisted
 
 let map_clb f = function
-  | Cltyp cfl -> Cltyp (map_fl f cfl)
-  | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2)
+  | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl)
+  | Clval (na,cfl1,cfl2) -> Clval (na,map_fl f cfl1,map_fl f cfl2)
+
+(* name of defined is erased (but it is pretty-printed) *)
+let clb_name = function
+    Cltyp(na,_) -> na
+  | Clval _ -> Anonymous
 
 (***********************)
                                                                                
 module Metaset = Intset
                                                                                
-let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false
+let meta_exists p s = Metaset.fold (fun x b -> b || (p x)) s false
 
 module Metamap = Intmap
 
-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 []
- 
 (*************************)
 (* Unification state *)
 
@@ -201,20 +202,23 @@ type conv_pb =
   | CONV 
   | CUMUL
 
-type meta_map = clbinding Metamap.t
 type evar_constraint = conv_pb * constr * constr
 type evar_defs =
     { evars : evar_map;
       conv_pbs : evar_constraint list;
       history : (existential_key * (loc * hole_kind)) list;
-      metas : meta_map }
+      metas : clbinding Metamap.t }
+
+let subst_evar_defs sub evd =
+  { evd with
+    conv_pbs =
+      List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2))
+        evd.conv_pbs;
+    metas = Metamap.map (map_clb (subst_mps sub)) evd.metas }
 
-let mk_evar_defs (sigma,mmap) =
-  { evars=sigma; conv_pbs=[]; history=[]; metas=mmap }
 let create_evar_defs sigma =
-  mk_evar_defs (sigma,Metamap.empty)
+  { evars=sigma; conv_pbs=[]; history=[]; metas=Metamap.empty }
 let evars_of d = d.evars
-let metas_of d = d.metas
 let evars_reset_evd evd d = {d with evars = evd}
 let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
@@ -225,7 +229,7 @@ let evar_source ev d =
 (* define the existential of section path sp as the constr body *)
 let evar_define sp body isevars =
   (* needed only if an inferred type *)
-  let body = Termops.refresh_universes body in
+  let body = refresh_universes body in
   {isevars with evars = define isevars.evars sp body}
 
 
@@ -235,8 +239,6 @@ let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd =
       {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty};
     history = (evn,src)::evd.history }
 
-let set_evar_source ev k evd = {evd with history=(ev,k)::evd.history}
-
 let is_defined_evar isevars (n,_) = is_defined isevars.evars n
 
 (* Does k corresponds to an (un)defined existential ? *)
@@ -245,6 +247,8 @@ let is_undefined_evar isevars c = match kind_of_term c with
   | _ -> false
 
 
+(* extracts conversion problems that satisfy predicate p *)
+(* Note: conv_pbs not satisying p are stored back in reverse order *)
 let get_conv_pbs isevars p =
   let (pbs,pbs1) = 
     List.fold_left
@@ -259,6 +263,11 @@ let get_conv_pbs isevars p =
   {isevars with conv_pbs = pbs1},
   pbs
 
+(**********************************************************)
+(* Accessing metas *)
+
+let meta_list evd = metamap_to_list evd.metas
+
 let meta_defined evd mv =
   match Metamap.find mv evd.metas with
     | Clval _ -> true
@@ -266,23 +275,98 @@ let meta_defined evd mv =
  
 let meta_fvalue evd mv =
   match Metamap.find mv evd.metas with
-    | Clval(b,_) -> b
+    | Clval(_,b,_) -> b
     | Cltyp _ -> anomaly "meta_fvalue: meta has no value"
            
 let meta_ftype evd mv =
   match Metamap.find mv evd.metas with
-    | Cltyp b -> b
-    | Clval(_,b) -> b
+    | Cltyp (_,b) -> b
+    | Clval(_,_,b) -> b
  
-let meta_declare mv v evd =
-  { evd with metas = Metamap.add mv (Cltyp(mk_freelisted v)) evd.metas }
+let meta_declare mv v ?(name=Anonymous) evd =
+  { evd with metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas }
   
 let meta_assign mv v evd =
-  {evd with
-    metas =
-      Metamap.add mv (Clval(mk_freelisted v, meta_ftype evd mv)) evd.metas }
+  match Metamap.find mv evd.metas with
+      Cltyp(na,ty) ->
+        { evd with
+          metas = Metamap.add mv (Clval(na,mk_freelisted v, ty)) evd.metas }
+    | _ -> anomaly "meta_assign: already defined"
+
+let meta_name evd mv =
+  try clb_name (Metamap.find mv evd.metas)
+  with Not_found -> Anonymous
+
+let meta_with_name evd id =
+  let na = Name id in
+  let mvl =
+    Metamap.fold (fun n clb l -> if clb_name clb = na then n::l else l)
+      evd.metas [] in
+  match mvl with
+    | []  -> 
+	errorlabstrm "Evd.meta_with_name"
+          (str"No such bound variable " ++ pr_id id)
+    | [n] -> 
+	n
+    |  _  -> 
+	 errorlabstrm "Evd.meta_with_name"
+           (str "Binder name \"" ++ pr_id id ++
+            str"\" occurs more than once in clause")
+
 
 let meta_merge evd1 evd2 =
   {evd2 with
     metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) 
       evd2.metas (metamap_to_list evd1.metas) }
+
+
+(**********************************************************)
+(* Pretty-printing *)
+
+let pr_meta_map mmap =
+  let pr_name = function
+      Name id -> str"[" ++ pr_id id ++ str"]"
+    | _ -> mt() in
+  let pr_meta_binding = function
+    | (mv,Cltyp (na,b)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name na ++ str " : " ++
+           print_constr b.rebus ++ fnl ())
+    | (mv,Clval(na,b,_)) ->
+      	hov 0 
+	  (pr_meta mv ++ pr_name na ++ str " := " ++
+           print_constr b.rebus ++ fnl ())
+  in
+  prlist pr_meta_binding (metamap_to_list mmap)
+
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+
+let pr_evar_info evi =
+  let phyps = pr_idl (List.rev (ids_of_named_context evi.evar_hyps)) in
+  let pty = print_constr evi.evar_concl in
+  let pb =
+    match evi.evar_body with
+      | Evar_empty -> mt ()
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+  in
+  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
+
+let pr_evar_map sigma =
+  h 0 
+    (prlist_with_sep pr_fnl
+      (fun (ev,evi) ->
+        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+      (to_list sigma))
+
+let pr_evar_defs evd =
+  let pp_evm =
+    if evd.evars = empty then mt() else
+      str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in
+  let n = List.length evd.conv_pbs in
+  let cstrs =
+    if n=0 then mt() else
+      str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in
+  let pp_met =
+    if evd.metas = Metamap.empty then mt() else
+      str"METAS:"++brk(0,1)++pr_meta_map evd.metas in
+  v 0 (pp_evm ++ cstrs ++ pp_met)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fd6e944e14..4487c92209 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -66,11 +66,11 @@ val existential_value : evar_map -> existential -> constr
 val existential_type : evar_map -> existential -> types
 val existential_opt_value : evar_map -> existential -> constr option
 
-(*************************)
+(*********************************************************************)
 (* constr with holes *)
 type open_constr = evar_map * constr
 
-(*************************)
+(*********************************************************************)
 (* The type constructor ['a sigma] adds an evar map to an object of
   type ['a] *)
 type 'a sigma = {
@@ -80,19 +80,13 @@ type 'a sigma = {
 val sig_it  : 'a sigma -> 'a
 val sig_sig : 'a sigma -> evar_map
 
-(*************************)
+(*********************************************************************)
 (* Meta map *)
 
 module Metaset : Set.S with type elt = metavariable
 
 val meta_exists : (metavariable -> bool) -> Metaset.t -> bool
 
-module Metamap : Map.S with type key = metavariable
-
-val metamap_in_dom : metavariable -> 'a Metamap.t -> bool
-val metamap_to_list : 'a Metamap.t -> (metavariable * 'a) list
-val metamap_inv : 'a Metamap.t -> 'a -> metavariable list
-
 type 'a freelisted = {
   rebus : 'a;
   freemetas : Metaset.t }
@@ -101,16 +95,24 @@ val mk_freelisted : constr -> constr freelisted
 val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 
 type clbinding =
-  | Cltyp of constr freelisted
-  | Clval of constr freelisted * constr freelisted
+  | Cltyp of name * constr freelisted
+  | Clval of name * constr freelisted * constr freelisted
 
 val map_clb : (constr -> constr) -> clbinding -> clbinding
 
-type meta_map = clbinding Metamap.t
-
-(*************************)
+(*********************************************************************)
 (* Unification state *)
+type evar_defs
 
+(* Substitution is not applied to the evar_map *)
+val subst_evar_defs : substitution -> evar_defs -> evar_defs
+
+(* create an evar_defs with empty meta map: *)
+val create_evar_defs : evar_map -> evar_defs
+val evars_of         : evar_defs -> evar_map
+val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
+
+(* Evars *)
 type hole_kind =
   | ImplicitArg of global_reference * (int * identifier option)
   | BinderType of name
@@ -118,40 +120,42 @@ type hole_kind =
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
+val is_defined_evar :  evar_defs -> existential -> bool
+val is_undefined_evar :  evar_defs -> constr -> bool
+val evar_declare :
+  named_context -> evar -> types -> ?src:loc * hole_kind ->
+  evar_defs -> evar_defs
+val evar_define : evar -> constr -> evar_defs -> evar_defs
+val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
+(* Unification constraints *)
 type conv_pb = 
   | CONV 
   | CUMUL
-
-type evar_defs
-val evars_of : evar_defs -> evar_map
-val metas_of : evar_defs -> meta_map
-
-val mk_evar_defs :  evar_map * meta_map -> evar_defs
-(* the same with empty meta map: *)
-val create_evar_defs :  evar_map -> evar_defs
-val evars_reset_evd :  evar_map ->  evar_defs -> evar_defs
-val reset_evd :  evar_map * meta_map ->  evar_defs -> evar_defs
-val evar_source : existential_key -> evar_defs -> loc * hole_kind
-
 type evar_constraint = conv_pb * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
-
-val evar_declare :
-  named_context -> evar -> types -> ?src:loc * hole_kind ->
-  evar_defs -> evar_defs
-val evar_define : evar -> constr -> evar_defs -> evar_defs
-
-val is_defined_evar :  evar_defs -> existential -> bool
-val is_undefined_evar :  evar_defs -> constr -> bool
-
 val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> 
   evar_defs * evar_constraint list
 
+(* Metas *)
+val meta_list : evar_defs -> (metavariable * clbinding) list
 val meta_defined : evar_defs -> metavariable -> bool
-val meta_fvalue   : evar_defs -> metavariable -> constr freelisted
-val meta_ftype    : evar_defs -> metavariable -> constr freelisted
-val meta_declare : metavariable -> types -> evar_defs -> evar_defs
-val meta_assign  : metavariable -> constr -> evar_defs -> evar_defs
-
+(* [meta_fvalue] raises Not_found if meta not in map or Anomaly if
+   meta has no value *)  
+val meta_fvalue    : evar_defs -> metavariable -> constr freelisted
+val meta_ftype     : evar_defs -> metavariable -> constr freelisted
+val meta_name      : evar_defs -> metavariable -> name
+val meta_with_name : evar_defs -> identifier -> metavariable
+val meta_declare   :
+  metavariable -> types -> ?name:name -> evar_defs -> evar_defs
+val meta_assign    : metavariable -> constr -> evar_defs -> evar_defs
+
+(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
 val meta_merge : evar_defs -> evar_defs -> evar_defs
+
+(*********************************************************************)
+(* debug pretty-printer: *)
+
+val pr_evar_info : evar_info -> Pp.std_ppcmds
+val pr_evar_map  : evar_map -> Pp.std_ppcmds
+val pr_evar_defs : evar_defs -> Pp.std_ppcmds
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9372effebd..3b0c1d6420 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -710,3 +710,27 @@ let is_info_type env sigma t =
   (s = Prop Pos) ||
   (s <> Prop Null && 
    try info_arity env sigma t.utj_val with IsType -> true)
+
+(*************************************)
+(* Metas *)
+
+let meta_value evd mv = 
+  let rec valrec mv =
+    try
+      let b = meta_fvalue evd mv in
+      instance
+        (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
+        b.rebus
+    with Anomaly _ | Not_found -> 
+      mkMeta mv
+  in 
+  valrec mv
+
+let meta_instance env b =
+  let c_sigma =
+    List.map 
+      (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
+  in 
+  instance c_sigma b.rebus
+
+let nf_meta env c = meta_instance env (mk_freelisted c)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 9c70b1a404..9f0a73d053 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -184,3 +184,7 @@ val instance : (metavariable * constr) list -> constr -> constr
 val hnf : env -> 'a evar_map -> constr -> constr * constr list
 i*)
 val apprec :  state_reduction_function
+
+(*s Meta-related reduction functions *)
+val meta_instance : evar_defs -> constr freelisted -> constr
+val nf_meta       : evar_defs -> constr -> constr
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d8c85cf7af..d89d5a879c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -36,62 +36,107 @@ let pr_name = function
 
 let pr_sp sp = str(string_of_kn sp)
 
-let rec print_constr c = match kind_of_term c with
+let rec pr_constr c = match kind_of_term c with
   | Rel n -> str "#"++int n
   | Meta n -> str "Meta(" ++ int n ++ str ")"
   | Var id -> pr_id id
   | Sort s -> print_sort s
   | Cast (c,t) -> hov 1 
-      (str"(" ++ print_constr c ++ cut() ++
-       str":" ++ print_constr t ++ str")")
+      (str"(" ++ pr_constr c ++ cut() ++
+       str":" ++ pr_constr t ++ str")")
   | Prod (Name(id),t,c) -> hov 1
-      (str"forall " ++ pr_id id ++ str":" ++ print_constr t ++ str"," ++
-       spc() ++ print_constr c)
+      (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++
+       spc() ++ pr_constr c)
   | Prod (Anonymous,t,c) -> hov 0
-      (str"(" ++ print_constr t ++ str " ->" ++ spc() ++
-       print_constr c ++ str")")
+      (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
+       pr_constr c ++ str")")
   | Lambda (na,t,c) -> hov 1
       (str"fun " ++ pr_name na ++ str":" ++
-       print_constr t ++ str" =>" ++ spc() ++ print_constr c)
+       pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
   | LetIn (na,b,t,c) -> hov 0
-      (str"let " ++ pr_name na ++ str":=" ++ print_constr b ++
-       str":" ++ brk(1,2) ++ print_constr t ++ cut() ++
-       print_constr c)
+      (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+       str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
+       pr_constr c)
   | App (c,l) ->  hov 1
-      (str"(" ++ print_constr c ++ spc() ++
-       prlist_with_sep spc print_constr (Array.to_list l) ++ str")")
+      (str"(" ++ pr_constr c ++ spc() ++
+       prlist_with_sep spc pr_constr (Array.to_list l) ++ str")")
   | Evar (e,l) -> hov 1
       (str"Evar#" ++ int e ++ str"{" ++
-       prlist_with_sep spc print_constr (Array.to_list l) ++str"}")
+       prlist_with_sep spc pr_constr (Array.to_list l) ++str"}")
   | Const c -> str"Cst(" ++ pr_sp c ++ str")"
   | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")"
   | Construct ((sp,i),j) ->
       str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")"
   | Case (ci,p,c,bl) -> v 0
-      (hv 0 (str"<"++print_constr p++str">"++ cut() ++ str"Case " ++
-             print_constr c ++ str"of") ++ cut() ++
-       prlist_with_sep (fun _ -> brk(1,2)) print_constr (Array.to_list bl) ++
+      (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++
+             pr_constr c ++ str"of") ++ cut() ++
+       prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++
       cut() ++ str"end")
   | Fix ((t,i),(lna,tl,bl)) ->
       let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in
       hov 1
         (str"fix " ++ int i ++ spc() ++  str"{" ++
          v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
-           pr_name na ++ str"/" ++ int i ++ str":" ++ print_constr ty ++
-           cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++
+           pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
   | CoFix(i,(lna,tl,bl)) ->
       let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in
       hov 1
         (str"cofix " ++ int i ++ spc() ++  str"{" ++
          v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
-           pr_name na ++ str":" ++ print_constr ty ++
-           cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++
+           pr_name na ++ str":" ++ pr_constr ty ++
+           cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref print_constr
+let term_printer = ref (fun _ -> pr_constr)
+let print_constr_env t = !term_printer t
+let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
 
+let pr_var_decl env (id,c,typ) =
+  let pbody = match c with
+    | None ->  (mt ())
+    | Some c ->
+	(* Force evaluation *) 
+	let pb = print_constr_env env c in
+	(str" := " ++ pb ++ cut () ) in
+  let pt = print_constr_env env typ in
+  let ptyp = (str" : " ++ pt) in
+  (pr_id id ++ hov 0 (pbody ++ ptyp))
+(*
+let pr_rel_decl env (na,c,typ) =
+  let pbody = match c with
+    | None -> mt ()
+    | Some c ->
+	(* Force evaluation *) 
+	let pb = prterm_env env c in
+	(str":=" ++ spc () ++ pb ++ spc ()) in
+  let ptyp = prtype_env env typ in
+  match na with
+  | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+  | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+*)
+let print_named_context env =
+  hv 0 (fold_named_context
+	  (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d)
+          env ~init:(mt ()))
+(*
+let pr_env env =
+  let sign_env =
+    fold_named_context
+      (fun env d pps ->
+         let pidt =  pr_var_decl env d in (pps ++ fnl () ++ pidt))
+      env ~init:(mt ()) 
+  in
+  let db_env =
+    fold_rel_context
+      (fun env d pps ->
+         let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat))
+      env ~init:(mt ())
+  in 
+  (sign_env ++ db_env)
+*)
 (*let current_module = ref empty_dirpath
 
 let set_module m = current_module := m*)
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index e1a9d5ba95..adc0e6daa6 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -27,8 +27,10 @@ val refresh_universes : types -> types
 val print_sort : sorts -> std_ppcmds
 val print_sort_family : sorts_family -> std_ppcmds
 (* debug printer: do not use to display terms to the casual user... *)
-val print_constr : constr -> std_ppcmds
-val set_print_constr : (constr -> std_ppcmds) -> unit
+val set_print_constr : (env -> constr -> std_ppcmds) -> unit
+val print_constr     : constr -> std_ppcmds
+val print_constr_env : env -> constr -> std_ppcmds
+val print_named_context : env -> std_ppcmds
 
 (* iterators on terms *)
 val prod_it : init:types -> (name * types) list -> types
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 9aa2758a03..759a0c1a15 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -18,6 +18,12 @@ open Pretype_errors
 open Inductive
 open Typeops
 
+let meta_type env mv =
+  let ty =
+    try Evd.meta_ftype env mv
+    with Not_found -> error ("unknown meta ?"^string_of_int mv) in
+  meta_instance env ty
+
 let vect_lift = Array.mapi lift
 let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 
@@ -38,7 +44,7 @@ let check_type env evd j ty =
 let rec execute env evd cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = Evarutil.meta_type evd n }
+        { uj_val = cstr; uj_type = meta_type evd n }
 
     | Evar ev ->
         let sigma = Evd.evars_of evd in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index c4503f51bd..dbb416beed 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -28,6 +28,7 @@ val check   : env -> evar_map -> constr -> types -> unit
 val mtype_of : env -> evar_defs -> constr -> types
 val msort_of : env -> evar_defs -> types -> sorts
 val mcheck   : env -> evar_defs -> constr -> types -> unit
+val meta_type : evar_defs -> metavariable -> types
  
 (* unused typing function... *)
 val mtype_of_type : env -> evar_defs -> types -> types
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 11b24f0964..d40c400680 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,40 +49,6 @@ let abstract_list_all env sigma typ c l =
 
 (*******************************)
 
-let w_Declare env sp ty evd =
-  let sigma = evars_of evd in
-  let _ = Typing.type_of env sigma ty in (* Checks there is no meta *)
-  let newdecl =
-    { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in 
-  evars_reset_evd (Evd.add sigma sp newdecl) evd
-
-(* [w_Define evd sp c]
- *
- * Defines evar [sp] with term [c] in evar context [evd].
- * [c] is typed in the context of [sp] and evar context [evd] with
- * [sp] removed to avoid circular definitions.
- * No unification is performed in order to assert that [c] has the
- * correct type.
- *)
-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";
-  let spdecl = Evd.map sigma sp in
-  let env = evar_env spdecl in
-  let _ =
-    (* Do not consider the metamap because evars may not depend on metas *)
-    try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl
-    with
-	Not_found -> error "Instantiation contains unlegal variables"
-      | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> 
-      errorlabstrm "w_Define"
-      (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ 
-       str (string_of_existential sp)) in
-  let spdecl' = { spdecl with evar_body = Evar_defined c } in
-  evars_reset_evd (Evd.add sigma sp spdecl') evd
-
-
 (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
    renvoie deux listes:
 
@@ -275,7 +241,7 @@ let w_merge env with_types metas evars evd =
     	  else
             begin
 	      if with_types (* or occur_meta mvty *) then
-	        (let mvty = meta_type evd mv in
+	        (let mvty = Typing.meta_type evd mv in
 		try 
                   let sigma = evars_of evd in
                   (* why not typing with the metamap ? *)
@@ -426,7 +392,7 @@ let secondOrderAbstraction env allow_K typ (p, oplist) evd =
   let sigma = evars_of evd in
   let (evd',cllist) =
     w_unify_to_subterm_list env allow_K oplist typ evd in
-  let typp = meta_type evd' p in
+  let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env sigma typp typ cllist in
   w_unify_0 env CONV (mkMeta p) pred evd'
 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 95b35a56ca..fb2a7ebbd6 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -9,18 +9,11 @@
 (*i $Id$ i*)
 
 (*i*)
-open Util
-open Names
 open Term
-open Sign
 open Environ
 open Evd
-open Evarutil
 (*i*)
 
-val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
-val w_Define : evar -> constr -> evar_defs -> evar_defs
-
 (* The "unique" unification fonction *)
 val w_unify :
   bool -> env -> conv_pb -> constr -> constr -> evar_defs -> evar_defs
@@ -35,6 +28,6 @@ val w_unify_to_subterm :
 
 (* [abstract_list_all env sigma t c l]                     *)
 (* abstracts the terms in l over c to get a term of type t *)
-(* (used in inv.ml) *)
+(* (exported for inv.ml) *)
 val abstract_list_all :
   env -> evar_map -> constr -> constr -> constr list -> constr