modules Evar_refiner et Typing_ev

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

19 files changed, 1401 insertions, 58 deletions

diff --git a/.depend b/.depend
index a44211446a..1c6ea061c3 100644
--- a/.depend
+++ b/.depend
@@ -51,6 +51,8 @@ parsing/pcoq.cmi: parsing/coqast.cmi
 parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
+proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/logic.cmi: kernel/environ.cmi kernel/evd.cmi proofs/proof_trees.cmi \
     kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: library/declare.cmi lib/pp.cmi proofs/proof_trees.cmi \
@@ -59,6 +61,10 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
     lib/util.cmi 
 proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi 
+proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \
+    kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
+    proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi 
+proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
@@ -236,16 +242,24 @@ parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi 
 parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi 
+proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \
+    proofs/typing_ev.cmi lib/util.cmi proofs/evar_refiner.cmi 
+proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx \
+    proofs/typing_ev.cmx lib/util.cmx proofs/evar_refiner.cmi 
 proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \
     lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/typeops.cmi kernel/typing.cmi lib/util.cmi \
-    proofs/logic.cmi 
+    kernel/term.cmi kernel/typeops.cmi kernel/typing.cmi proofs/typing_ev.cmi \
+    lib/util.cmi proofs/logic.cmi 
 proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
     kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx lib/util.cmx \
-    proofs/logic.cmi 
+    kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx proofs/typing_ev.cmx \
+    lib/util.cmx proofs/logic.cmi 
 proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
     lib/util.cmi proofs/proof_trees.cmi 
@@ -260,6 +274,16 @@ proofs/refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/instantiate.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_trees.cmx \
     kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \
     lib/util.cmx proofs/refiner.cmi 
+proofs/tacmach.cmo: proofs/tacmach.cmi 
+proofs/tacmach.cmx: proofs/tacmach.cmi 
+proofs/tacred.cmo: proofs/tacred.cmi 
+proofs/tacred.cmx: proofs/tacred.cmi 
+proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
+    kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
+    kernel/typeops.cmi lib/util.cmi proofs/typing_ev.cmi 
+proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
+    kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
+    kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
@@ -306,33 +330,3 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmi \
     toplevel/vernac.cmi 
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernac.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
-    toplevel/vernac.cmx 
-parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi 
-parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
-    lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    parsing/g_minicoq.cmi 
-parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
-    lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    parsing/g_minicoq.cmi 
-parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/pcoq.cmi 
-parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmi 
-parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
-    lib/pp.cmx 
-parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
-parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx 
-parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
-    lib/util.cmi parsing/pcoq.cmi 
-parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
-    lib/util.cmx parsing/pcoq.cmi 
-parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
diff --git a/.depend.camlp4 b/.depend.camlp4
new file mode 100644
index 0000000000..f1671b6ba3
--- /dev/null
+++ b/.depend.camlp4
@@ -0,0 +1,30 @@
+parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    toplevel/vernac.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
+    toplevel/vernac.cmx 
+parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    parsing/g_minicoq.cmi 
+parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
+    lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+    parsing/g_minicoq.cmi 
+parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \
+    parsing/pcoq.cmi 
+parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
+    parsing/pcoq.cmi 
+parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
+    lib/pp.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
+    lib/pp.cmx 
+parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
+parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx 
+parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
+    lib/util.cmi parsing/pcoq.cmi 
+parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
+    lib/util.cmx parsing/pcoq.cmi 
+parsing/q_coqast.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/q_coqast.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
diff --git a/Makefile b/Makefile
index 09b189ca0e..465268ad0f 100644
--- a/Makefile
+++ b/Makefile
@@ -51,7 +51,8 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
 	parsing/g_prim.cmo parsing/g_basevernac.cmo parsing/g_vernac.cmo \
 	parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo
 
-PROOFS=proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo
+PROOFS=proofs/typing_ev.cmo proofs/proof_trees.cmo proofs/logic.cmo \
+       proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
@@ -207,13 +208,19 @@ cleanconfig::
 
 # Dependencies
 
+alldepend: depend dependcamlp4
+
 depend: beforedepend
 	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
+
+dependcamlp4: beforedepend
+	rm -f .depend.camlp4
 	for f in */*.ml4; do \
 	  file=`dirname $$f`/`basename $$f .ml4`; \
 	  camlp4o $(INCLUDES) pa_extend.cmo q_MLast.cmo $(GRAMMARCMO) pr_o.cmo -impl $$f > $$file.ml; \
-	  ocamldep $(DEPFLAGS) $$file.ml >> .depend; \
+	  ocamldep $(DEPFLAGS) $$file.ml >> .depend.camlp4; \
 	  rm -f $$file.ml; \
 	done
 
 include .depend
+include .depend.camlp4
\ No newline at end of file
diff --git a/dev/TODO b/dev/TODO
index 0ec070bc2b..8f5fb1ddf9 100644
--- a/dev/TODO
+++ b/dev/TODO
@@ -6,8 +6,6 @@
  o Variables existentielles
      - traiter le constructeur Evar dans les fonctions de réductions
        (parallèlement à Const)
-     - ajouter dans Environ des fonctions d'introduction et de recherche
-       des ve
      - unifier Meta et Evar
 
  o Lib
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 3e33dca7b7..6b38b72ff6 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -301,6 +301,24 @@ let occur_oper s =
   in 
   occur_rec 
 
+let process_opers_of_term p f l constr = 
+  let rec filtrec acc = function
+    | DOP0 oper        -> if p oper then ((f oper)::acc) else acc
+    | VAR _            -> acc
+    | DOP1(oper,c)     -> let newacc = filtrec acc c in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOP2(oper,c1,c2) -> let newacc = filtrec (filtrec acc c1) c2 in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOPN(oper,cl)    -> let newacc = (Array.fold_left filtrec acc cl) in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DOPL(oper,cl)    -> let newacc = (List.fold_left filtrec acc cl) in
+                          if p oper then ((f oper)::newacc) else newacc
+    | DLAM(_,c)        -> filtrec acc c
+    | DLAMV(_,v)       -> Array.fold_left filtrec acc v
+    | _                -> acc
+  in 
+  filtrec l constr
+
 (* Returns the list of global variables in a term *)
 
 let global_varsl l constr = 
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 49ec5bfbe5..cad600a50c 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -81,6 +81,8 @@ val occur_opern : 'a -> 'a term -> bool
 val occur_oper0 : 'a -> 'a term -> bool
 val occur_var : identifier -> 'a term -> bool
 val occur_oper : 'a -> 'a term -> bool
+val process_opers_of_term : 
+  ('a -> bool) -> ('a -> 'b) -> 'b list -> 'a term -> 'b list
 val dependent : 'a term -> 'a term -> bool
 val global_varsl : identifier list -> 'a term -> identifier list
 val global_vars : 'a term -> identifier list
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ac32e2eabd..7119729c7d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1425,3 +1425,5 @@ let rec strip_all_casts t =
     | DLAMV(na,c) -> DLAMV(na,Array.map (under_outer_cast strip_all_casts) c)
     | VAR _ as t -> t
     | Rel _ as t -> t
+
+
diff --git a/lib/util.ml b/lib/util.ml
index 0f900ff923..62a86b55f5 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -146,6 +146,11 @@ let list_try_find_i f =
   in 
   try_find_f
 
+let rec list_uniquize = function
+  | [] -> []
+  | h::t -> if List.mem h t then list_uniquize t else h::(list_uniquize t)
+
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index 7998dde2a2..4075a70451 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -44,6 +44,7 @@ val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
+val list_uniquize : 'a list -> 'a list
 
 (*s Arrays. *)
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
new file mode 100644
index 0000000000..f3421cfdcc
--- /dev/null
+++ b/proofs/evar_refiner.ml
@@ -0,0 +1,160 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Stamps
+open Names
+open Generic
+open Term
+open Environ
+open Evd
+open Reduction
+open Typing_ev
+open Proof_trees
+open Logic
+open Refiner
+
+let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
+let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it
+
+type walking_constraints = readable_constraints idstamped
+type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
+type w_tactic = walking_constraints -> walking_constraints
+
+
+let local_Constraints lc gs = refiner (Local_constraints lc) gs
+
+let on_wc f wc = ids_mod f wc
+
+let startWalk gls =
+  let evc = project_with_focus gls in
+  let wc = (ids_mk evc) in 
+  (wc,
+   (fun wc' gls' ->
+      if ids_eq wc wc' & gls.it = gls'.it then
+        if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then
+          tclIDTAC {it=gls'.it; sigma = get_gc (ids_it wc')}
+        else
+          (local_Constraints (get_focus (ids_it wc'))
+             {it=gls'.it; sigma = get_gc (ids_it wc')})
+      else error "Walking"))
+
+let walking_THEN wt rt gls =
+  let (wc,kONT) = startWalk gls in
+  let (wc',rslt) = wt wc in 
+  tclTHEN (kONT wc') (rt rslt) gls
+
+let walking wt = walking_THEN (fun wc -> (wt wc,())) (fun () -> tclIDTAC)
+
+let extract_decl sp evc =
+  let evdmap = (ts_it evc).decls in
+  let evd = Evd.map evdmap sp in 
+  (ts_mk { env = evd.evar_env;
+           focus = get_lc evd;
+           decls = Evd.rmv evdmap sp })
+
+let restore_decl sp evd evc =
+  let newctxt = { lc = (ts_it evc).focus;
+                  mimick = (get_mimick evd);
+                  pgm = (get_pgm evd) } in
+  let newgoal = { evar_env = evd.evar_env; 
+		  evar_concl = evd.evar_concl;
+		  evar_body = evd.evar_body;
+                  evar_info = newctxt } in
+  (rc_add evc (sp,newgoal))
+
+
+(* [w_Focusing sp wt wc]
+ *
+ * Focuses the walking context WC onto the declaration SP, given that
+ * this declaration is UNDEFINED.  Then, it runs the walking_tactic,
+ * WT, on this new context.  When the result is returned, we recover
+ * the resulting focus (access list) and restore it to SP's declaration.
+ *
+ * It is an error to cause SP to change state while we are focused on it. *)
+
+let w_Focusing_THEN sp (wt:'a result_w_tactic) (wt':'a -> w_tactic)
+                       (wc:walking_constraints) =
+  let focus = (ts_it (ids_it wc)).focus
+  and env  = (ts_it (ids_it wc)).env
+  and evd   = Evd.map (ts_it (ids_it wc)).decls sp in
+  let (wc':walking_constraints) = ids_mod (extract_decl sp) wc in
+  let (wc'',rslt) = wt wc' in 
+  if not (ids_eq wc wc'') then error "w_saving_focus";
+  if ts_eq (ids_it wc') (ids_it wc'') then 
+    wt' rslt wc
+  else 
+    let wc''' = ids_mod (restore_decl sp evd) wc'' in 
+    wt' rslt
+      (ids_mod
+         (ts_mod (fun evc ->
+                    { env = env;
+                      focus = focus;
+                      decls = evc.decls }))
+         wc''')
+      
+let w_add_sign (id,t) (wc:walking_constraints) =
+  ids_mk (ts_mod
+            (fun evr ->
+               { focus = evr.focus;
+		 env = push_var (id,t) evr.env;
+		 decls = evr.decls })
+            (ids_it wc))
+
+let ctxt_type_of evc c = type_of (ts_it evc).env (ts_it evc).decls c
+
+let w_IDTAC wc = wc
+
+let w_Focusing sp wt = 
+  w_Focusing_THEN sp (fun wc -> (wt wc,())) (fun _ -> w_IDTAC)
+
+let w_Focus sp wc = ids_mod (extract_decl sp) wc
+
+let w_Underlying wc = (ts_it (ids_it wc)).decls
+let w_type_of wc c  = ctxt_type_of (ids_it wc) c
+let w_env     wc    = get_env (ids_it wc)
+let w_ORELSE wt1 wt2 wc = try wt1 wc with UserError _ -> wt2 wc
+
+let w_Declare sp c (wc:walking_constraints) =
+  begin match c with 
+    | DOP2(Cast,_,_) -> ()
+    | _ -> error "Cannot declare an un-casted evar"
+  end;
+  let _ = w_type_of wc c in
+  let access  = get_focus (ids_it wc)
+  and env = get_env (ids_it wc)in
+  let newdecl = mk_goal (mt_ctxt access) env c in 
+  ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints)
+
+let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c)
+
+let evars_of sigma c =
+  List.fold_right Intset.add 
+    (list_uniquize (process_opers_of_term
+             	      (function 
+			 | Evar ev -> Evd.in_dom (ts_it sigma).decls ev
+			 | _ -> false)
+             	      (function 
+			 | Evar ev -> ev
+	     		 | _ -> assert false) [] c))
+    Intset.empty
+
+let w_Define sp c wc =
+  let spdecl = Evd.map (w_Underlying wc) sp in
+  let cty = 
+    try 
+      ctxt_type_of (ids_it (w_Focus sp wc)) (DOP2(Cast,c,spdecl.evar_concl))
+    with Not_found -> 
+      error "Instantiation contains unlegal variables"
+  in 
+  match spdecl.evar_body with
+    | Evar_empty ->
+    	let access = evars_of (ids_it wc) c in
+    	let spdecl' = { evar_env = spdecl.evar_env;
+                       	evar_concl = spdecl.evar_concl;
+                       	evar_info = mt_ctxt access;
+                       	evar_body = Evar_defined c }
+    	in 
+	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
+    | _ -> error "define_evar"
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
new file mode 100644
index 0000000000..1136d54cf0
--- /dev/null
+++ b/proofs/evar_refiner.mli
@@ -0,0 +1,47 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Evd
+open Proof_trees
+open Refiner
+(*i*)
+
+val rc_of_pfsigma : proof_tree sigma -> readable_constraints
+val rc_of_glsigma : goal sigma -> readable_constraints
+
+type walking_constraints
+
+type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a
+type w_tactic           = walking_constraints -> walking_constraints
+
+val local_Constraints : 
+  local_constraints -> goal sigma -> goal list sigma * validation
+
+val startWalk : 
+  goal sigma -> walking_constraints * (walking_constraints -> tactic)
+
+val walking_THEN    : 'a result_w_tactic -> ('a -> tactic) -> tactic
+val walking         : w_tactic -> tactic
+val w_Focusing_THEN : 
+  evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic
+
+val w_Declare    : evar -> constr -> w_tactic
+val w_Declare_At : evar -> evar -> constr -> w_tactic
+val w_Define     : evar -> constr -> w_tactic
+
+val w_Underlying : walking_constraints -> evar_declarations
+val w_env        : walking_constraints -> unsafe_env
+val w_type_of    : walking_constraints -> constr -> constr
+val w_add_sign   : (identifier * typed_type) -> walking_constraints 
+                     -> walking_constraints
+
+val w_IDTAC      : w_tactic
+val w_ORELSE     : w_tactic -> w_tactic -> w_tactic
+val ctxt_type_of : readable_constraints -> constr -> constr
+
+val evars_of     : readable_constraints -> constr -> local_constraints
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e6f07410bd..a52e8603d1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -10,6 +10,7 @@ open Term
 open Sign
 open Environ
 open Reduction
+open Typing_ev
 open Proof_trees
 open Typeops
 open Coqast
@@ -26,12 +27,6 @@ let conv_leq_goal env sigma arg ty conclty =
   if not (is_conv_leq env sigma ty conclty) then 
     raise (RefinerError (BadType (arg,ty,conclty)))
 
-let type_of env c =
-  failwith "TODO: typage avec VE"
-
-let execute_type env ty =
-  failwith "TODO: typage type avec VE"
-
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = goal.evar_env in
   match trm with
@@ -42,7 +37,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
-	let _ = type_of env ty in
+	let _ = type_of env sigma ty in
 	conv_leq_goal env sigma trm ty conclty;
 	mk_refgoals sigma goal goalacc ty t
 
@@ -66,7 +61,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 
     | t -> 
 	if occur_meta t then raise (RefinerError (OccurMeta t));
-      	let t'ty = type_of env t in
+      	let t'ty = type_of env sigma t in
 	conv_leq_goal env sigma t t'ty conclty;
         (goalacc,t'ty)
 
@@ -77,7 +72,7 @@ and mk_hdgoals sigma goal goalacc trm =
   let env = goal.evar_env in
   match trm with
     | DOP2(Cast,DOP0(Meta mv),ty) ->
-	let _ = type_of env ty in
+	let _ = type_of env sigma ty in
 	let ctxt = goal.evar_info in  
 	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
 	  
@@ -95,7 +90,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	in
 	(acc'',conclty')
 
-    | t -> goalacc,type_of env t
+    | t -> goalacc, type_of env sigma t
 
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
@@ -142,7 +137,7 @@ let new_meta_variables =
   in 
   newrec
 
-let mk_assumption env c = execute_type env c
+let mk_assumption env sigma c = execute_type env sigma c
 				   
 let sign_before id = 
   let rec aux = function
@@ -222,7 +217,7 @@ let prim_refiner r sigma goal =
         (match strip_outer_cast cl with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = mk_assumption env sign c1
+	       let a = mk_assumption env sigma c1
 	       and v = VAR id in
 	       let sg = mk_goal info (push_var (id,a) env) (sAPP b v) in 
 	       [sg]
@@ -238,7 +233,7 @@ let prim_refiner r sigma goal =
                          (global_vars c1)) then
 		 error 
 		   "Can't introduce at that location: free variable conflict";
-	       let a = mk_assumption env sign c1
+	       let a = mk_assumption env sigma c1
 	       and v = VAR id in
 	       let env' = change_hyps (add_sign_after whereid (id,a)) env in
 	       let sg = mk_goal info env' (sAPP b v) in 
@@ -257,7 +252,7 @@ let prim_refiner r sigma goal =
 	       then 
 		 error 
 		   "Can't introduce at that location: free variable conflict";
-	       let a = mk_assumption env sign c1
+	       let a = mk_assumption env sigma c1
 	       and v = VAR id in
 	       let env' = change_hyps (add_sign_replacing id (id,a)) env in
 	       let sg = mk_goal info env' (sAPP b v) in
@@ -280,7 +275,7 @@ let prim_refiner r sigma goal =
 	in
      	let _ = check_ind n cl in 
 	if mem_sign sign f then error "name already used in the environment";
-        let a = mk_assumption env sign cl in
+        let a = mk_assumption env sigma cl in
         let sg = mk_goal info (push_var (f,a) env) cl in
         [sg]
     
@@ -307,7 +302,7 @@ let prim_refiner r sigma goal =
 		       "mutual inductive declaration");
 	      if mem_sign sign f then 
 		error "name already used in the environment";
-	      let a = mk_assumption env sign ar in
+	      let a = mk_assumption env sigma ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
 	      List.map (mk_goal info env) (cl::lar)
@@ -331,7 +326,7 @@ let prim_refiner r sigma goal =
           | (ar::lar'),(f::lf') ->
 	      if mem_sign sign f then 
 		error "name already used in the environment";
-	      let a = mk_assumption env sign ar in
+	      let a = mk_assumption env sigma ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf')
 	  | ([],[]) -> List.map (mk_goal info env) (cl::lar)
 	  | _ -> error "not the right number of arguments"
@@ -345,7 +340,7 @@ let prim_refiner r sigma goal =
 	sgl
 
     | { name = Convert_concl; terms = [cl'] } ->
-    	let cl'ty = type_of env sign cl' in
+    	let cl'ty = type_of env sigma cl' in
 	if is_conv_leq env sigma cl' cl then
           let sg = mk_goal info env (DOP2(Cast,cl',cl'ty)) in
           [sg]
@@ -354,7 +349,8 @@ let prim_refiner r sigma goal =
 
     | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } ->
       (* Faut-il garder la sorte d'origine ou celle du converti ?? *)
-    	let tj = execute_type env (sign_before id sign) ty' in
+	let env' = change_hyps (sign_before id) env in
+    	let tj = execute_type env' sigma ty' in
 	if is_conv env sigma ty' (snd(lookup_sign id sign)).body then
 	  let env' = change_hyps (modify_sign id tj) env in
           [mk_goal info env' cl]
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index b2d59fe63c..1e7caa6a03 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -130,7 +130,7 @@ type global_constraints = evar_declarations timestamped
 
 type evar_recordty = {
   focus : local_constraints;
-  env  : unsafe_env;
+  env   : unsafe_env;
   decls : evar_declarations }
 
 and readable_constraints = evar_recordty timestamped
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
new file mode 100644
index 0000000000..c4c8dc6ed2
--- /dev/null
+++ b/proofs/tacmach.ml
@@ -0,0 +1,479 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Evd
+open Term
+open Reduction
+open Himsg
+open Termenv
+open Termast
+open CoqAst
+open Trad
+open Proof_trees
+open Printer
+
+open Logic
+open Evar_refiner
+open Refiner
+
+
+type 'a sigma = 'a Refiner.sigma
+
+type validation = proof_tree list -> proof_tree
+
+type tactic = goal sigma -> (goal list sigma * validation)
+
+let re_sig it gc = { it = it; sigma = gc }
+
+
+(**************************************************************)
+(* Operations for handling terms under a local typing context *)
+(**************************************************************)
+
+let unpackage = Refiner.unpackage
+let repackage = Refiner.repackage
+let apply_sig_tac = Refiner.apply_sig_tac
+
+let sig_it       = Refiner.sig_it
+let sig_sig      = Refiner.sig_sig
+let project      = (comp ts_it sig_sig)
+let pf_hyps gls  = (sig_it gls).hyps
+
+let pf_untyped_hyps gls  =
+  let (idl,tyl) = (sig_it gls).hyps in (idl, List.map (fun x -> x.body) tyl)
+
+let pf_concl gls = (sig_it gls).concl
+
+let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
+
+let pf_get_hyp gls id = 
+  try (snd (lookup_sign id (pf_untyped_hyps gls)))
+  with Not_found -> error ("No such hypothesis : " ^ (string_of_id id))
+
+let pf_ctxt gls      = get_ctxt (sig_it gls)
+
+let pf_type_of gls c =
+  Mach.type_of (ts_it (sig_sig gls)) (sig_it gls).hyps c
+
+let hnf_type_of gls = 
+  (comp (whd_betadeltaiota (project gls)) (pf_type_of gls))
+
+let pf_check_type gls c1 c2 =
+  let casted = mkCast c1 c2 in pf_type_of gls casted
+
+let pf_constr_of_com gls c =
+  let evc = project gls in 
+  constr_of_com evc (sig_it gls).hyps c
+
+let pf_constr_of_com_sort gls c =
+  let evc = project gls in 
+  constr_of_com_sort evc (sig_it gls).hyps c
+
+let pf_global gls id = Machops.global (gLOB (sig_it gls).hyps) id
+let pf_parse_const gls = comp (pf_global gls) id_of_string 
+
+			   
+(* We sould not call Mach in tactics *)
+let pf_fexecute gls =
+  let evc = project gls in 
+  Trad.ise_resolve true evc [] (gLOB (sig_it gls).hyps)
+
+let pf_infexecute gls =
+  let evc = project gls in
+  let sign = (sig_it gls).hyps in 
+  Mach.infexecute evc (sign, Mach.fsign_of_sign evc sign)
+
+let pf_reduction_of_redexp gls re c = 
+  reduction_of_redexp re (project gls) c 
+
+let pf_reduce redfun gls c       = redfun (project gls) c 
+let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
+let pf_whd_betadeltaiota_stack   = pf_reduce whd_betadeltaiota_stack
+let pf_hnf_constr                = pf_reduce hnf_constr
+let pf_red_product               = pf_reduce red_product
+let pf_nf                        = pf_reduce nf
+let pf_compute                   = pf_reduce compute
+let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
+
+let pf_conv_x                   = pf_reduce conv_x
+let pf_conv_x_leq               = pf_reduce conv_x_leq
+let pf_const_value              = pf_reduce const_value
+let pf_one_step_reduce          = pf_reduce one_step_reduce
+let pf_reduce_to_mind           = pf_reduce reduce_to_mind
+let pf_reduce_to_ind            = pf_reduce reduce_to_ind
+
+(************************************)
+(* Tactics handling a list of goals *)
+(************************************)
+
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+let first_goal         = first_goal
+let goal_goal_list     = goal_goal_list
+let apply_tac_list     = apply_tac_list
+let then_tactic_list   = then_tactic_list
+let tactic_list_tactic = tactic_list_tactic
+let tclFIRSTLIST       = tclFIRSTLIST
+let tclIDTAC_list      = tclIDTAC_list
+
+
+(********************************************************)
+(* Functions for handling the state of the proof editor *)
+(********************************************************)
+
+type pftreestate = Refiner.pftreestate
+
+let proof_of_pftreestate    = proof_of_pftreestate
+let cursor_of_pftreestate   = cursor_of_pftreestate
+let is_top_pftreestate      = is_top_pftreestate
+let evc_of_pftreestate      = evc_of_pftreestate
+let top_goal_of_pftreestate = top_goal_of_pftreestate
+let nth_goal_of_pftreestate = nth_goal_of_pftreestate
+let traverse                = traverse
+let solve_nth_pftreestate   = solve_nth_pftreestate
+let solve_pftreestate       = solve_pftreestate
+let weak_undo_pftreestate   = weak_undo_pftreestate
+let mk_pftreestate          = mk_pftreestate
+let extract_pftreestate     = extract_pftreestate
+let first_unproven          = first_unproven
+let last_unproven           = last_unproven
+let nth_unproven            = nth_unproven
+let node_prev_unproven      = node_prev_unproven
+let node_next_unproven      = node_next_unproven
+let next_unproven           = next_unproven
+let prev_unproven           = prev_unproven
+let top_of_tree             = top_of_tree
+let frontier                = frontier
+let change_constraints_pftreestate = change_constraints_pftreestate
+
+(***********************************)
+(* Walking constraints re-exported *)
+(***********************************)
+
+type walking_constraints = Evar_refiner.walking_constraints
+type 'a result_w_tactic  = walking_constraints -> walking_constraints * 'a
+type w_tactic            = walking_constraints -> walking_constraints
+
+let startWalk       = startWalk
+let walking_THEN    = walking_THEN
+let walking         = walking
+let w_Focusing_THEN = w_Focusing_THEN
+let w_Declare       = w_Declare
+let w_Declare_At    = w_Declare_At
+let w_Define        = w_Define
+let w_Underlying    = w_Underlying
+let w_hyps          = w_hyps
+let w_type_of       = w_type_of
+let w_IDTAC         = w_IDTAC
+let w_ORELSE        = w_ORELSE
+let w_add_sign      = w_add_sign
+let ctxt_type_of    = ctxt_type_of
+
+let w_defined_const wc k     = defined_const (w_Underlying wc) k
+let w_const_value wc         = const_value (w_Underlying wc)
+let w_conv_x wc m n          = conv_x (w_Underlying wc) m n
+let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_Underlying wc) c
+let w_hnf_constr wc c         = hnf_constr (w_Underlying wc) c
+
+
+(*************************************************)
+(* Tacticals re-exported from the Refiner module.*)
+(*************************************************)
+
+let tclIDTAC         = tclIDTAC
+let tclORELSE        = tclORELSE
+let tclTHEN          =  tclTHEN
+let tclTHEN_i        =  tclTHEN_i
+let tclTHENL         =  tclTHENL
+let tclTHENS         =  tclTHENS
+let tclTHENSI        =  tclTHENSI
+let tclREPEAT        =  tclREPEAT
+let tclFIRST         =  tclFIRST
+let tclSOLVE         =  tclSOLVE
+let tclTRY           =  tclTRY
+let tclTHENTRY       =  tclTHENTRY
+let tclCOMPLETE      =  tclCOMPLETE
+let tclAT_LEAST_ONCE =  tclAT_LEAST_ONCE
+let tclFAIL          =  tclFAIL
+let tclDO            =  tclDO
+let tclPROGRESS      =  tclPROGRESS
+let tclWEAK_PROGRESS = tclWEAK_PROGRESS
+let tclNOTSAMEGOAL = tclNOTSAMEGOAL
+let tclINFO          =  tclINFO
+
+let unTAC            = unTAC
+
+
+(********************************************)
+(* Definition of the most primitive tactics *)
+(********************************************)
+
+let refiner = refiner
+
+let introduction id pf =
+  refiner (Prim { name = Intro; newids = [id];
+                  hypspecs = []; terms = []; params = [] }) pf
+
+let intro_replacing whereid pf = 
+  refiner (Prim { name = Intro_replacing; newids = [];
+                  hypspecs = [whereid]; terms = []; params = [] }) pf
+
+let refine c pf = 
+  refiner (Prim { name = Refine; terms = [c];
+		  hypspecs = []; newids = []; params = [] }) pf
+
+let convert_concl c pf = 
+  refiner (PRIM{name=CONVERT_CONCL;terms=[c];
+                hypspecs=[];newids=[];params=[]}) pf
+
+let convert_hyp id c pf = 
+  refiner (PRIM{name=CONVERT_HYP;hypspecs=[id];
+                terms=[c];newids=[];params=[]}) pf
+
+let thin ids gl = 
+  refiner (PRIM{name=THIN;hypspecs=ids;
+                terms=[];newids=[];params=[]}) gl
+
+let move_hyp with_dep id1 id2 gl = 
+  refiner (PRIM{name=MOVE with_dep;
+                hypspecs=[id1;id2];terms=[];newids=[];params=[]}) gl
+
+let mutual_fix lf ln lar pf = 
+  refiner (PRIM{name=FIX;newids=lf;
+                hypspecs=[];terms=lar;
+                params=List.map num ln}) pf
+
+let mutual_cofix lf lar pf = 
+  refiner (PRIM{name     = COFIX;
+                newids   = lf;
+                hypspecs = [];
+                terms    = lar; 
+                params   = []}) pf
+    
+let rename_bound_var_goal gls =
+  let ({hyps=sign;concl=cl} as gl) = (sig_it gls) in 
+  convert_concl (rename_bound_var (ids_of_sign sign) cl) gls
+
+
+(***************************************)
+(* The interpreter of defined tactics *)
+(***************************************)
+
+let vernac_tactic = vernac_tactic
+let context       = context
+
+
+(************************************************************************)
+(* A generic tactic registration function with a default tactic printer *)
+(************************************************************************)
+
+(* A generic tactic printer *)
+
+let pr_com sigma goal com =
+  prterm (rename_bound_var 
+            (ids_of_sign goal.hyps) 
+            (Trad.constr_of_com sigma goal.hyps com))
+    
+let pr_one_binding sigma goal = function
+  | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]
+  | (NoDep n,com) -> [< 'iNT n ; 'sTR":=" ; pr_com sigma goal com >]
+  | (Com,com)     -> [< pr_com sigma goal com >]
+
+let pr_bindings sigma goal lb =
+  let prf = pr_one_binding sigma goal in 
+  match lb with 
+    | [] -> [< prlist_with_sep pr_spc prf lb >]
+    | _  -> [<'sTR"with";'sPC;prlist_with_sep pr_spc prf lb >]
+
+let rec pr_list f = function
+  | []   -> [<>] 
+  | a::l1 -> [< (f a) ; pr_list f l1>]
+
+let pr_gls gls =
+  hOV 0 [< pr_decls (sig_sig gls) ; 'fNL ; pr_seq (sig_it gls) >]
+
+let pr_glls glls =
+  hOV 0 [< pr_decls (sig_sig glls) ; 'fNL ;
+           prlist_with_sep pr_fnl pr_seq (sig_it glls) >]
+
+let pr_tactic = Refiner.pr_tactic
+
+let add_tactic = Refiner.add_tactic
+
+let overwriting_tactic = Refiner.overwriting_add_tactic
+
+
+(********************************************************)
+(* Functions for hiding the implementation of a tactic. *)
+(********************************************************)
+
+let hide_tactic  s tac  =
+  add_tactic s tac;
+  (fun args -> vernac_tactic(s,args))
+
+
+let overwrite_hidden_tactic s tac  =
+  overwriting_add_tactic s tac;
+  (fun args -> vernac_tactic(s,args))
+
+(* Some combinators for parsing tactic arguments. 
+   They transform the CoqAst.t arguments of the tactic into 
+   constr arguments *)
+
+type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
+
+let tactic_com = 
+  fun tac t x -> tac (pf_constr_of_com x t) x
+      
+let tactic_com_sort = 
+  fun tac t x -> tac (pf_constr_of_com_sort x t) x
+      
+let tactic_com_list =
+  fun tac tl x -> 
+    let translate = pf_constr_of_com x in 
+    tac (List.map translate tl) x
+
+let tactic_bind_list =
+  fun tac tl x -> 
+    let translate = pf_constr_of_com x in 
+    tac (List.map (fun (b,c)->(b,translate c)) tl) x
+
+let tactic_com_bind_list =
+  fun tac (c,tl) x -> 
+    let translate = pf_constr_of_com x in 
+    tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x
+
+let tactic_com_bind_list_list =
+  fun tac args gl -> 
+    let translate (c,tl) = 
+      (pf_constr_of_com gl c,
+       List.map (fun (b,c')->(b,pf_constr_of_com gl c')) tl)
+    in 
+    tac (List.map translate args) gl
+
+
+(* Some useful combinators for hiding tactic implementations *)
+
+type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
+
+let hide_atomic_tactic s tac = 
+  add_tactic s (function [] -> tac | _ -> assert false);
+  vernac_tactic(s,[])
+
+let overwrite_hidden_atomic_tactic s tac =
+  overwriting_tactic s (function [] -> tac | _ -> assert false);
+  vernac_tactic(s,[])
+
+
+let hide_constr_comarg_tactic s tac =
+  let tacfun = function 
+    | [CONSTR c]    -> tac c
+    | [COMMAND com] -> tactic_com tac com
+    | _ -> anomaly "hide_constr_comarg_tactic : neither CONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  (fun c   -> vernac_tactic(s,[(CONSTR c)])), 
+  fun com -> vernac_tactic(s,[(COMMAND com)])
+ 
+let overwrite_hidden_constr_comarg_tactic s tac =
+  let tacfun = function 
+    | [CONSTR c] -> tac c
+    | [COMMAND com] -> 
+        (fun gls -> tac (pf_constr_of_com gls com) gls)
+    | _ -> 
+	anomaly 
+	  "overwrite_hidden_constr_comarg_tactic : neither CONSTR nor COMMAND"
+  in 
+  overwriting_tactic s tacfun;
+  (fun c -> vernac_tactic(s,[(CONSTR c)]), 
+   fun c -> vernac_tactic(s,[(COMMAND c)]))
+
+let hide_constr_tactic s tac =
+  let tacfun = function 
+    | [CONSTR c]    -> tac c
+    | [COMMAND com] -> tactic_com tac com
+    | _ -> anomaly "hide_constr_tactic : neither CONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  (fun c  -> vernac_tactic(s,[(CONSTR c)]))
+
+let hide_numarg_tactic s tac =
+  let tacfun = (function [INTEGER n] -> tac n | _ -> assert false) in 
+  add_tactic s tacfun;
+  fun n -> vernac_tactic(s,[INTEGER n])
+
+let hide_ident_tactic s tac =
+  let tacfun = (function [IDENTIFIER id] -> tac id | _ -> assert false) in
+  add_tactic s tacfun;
+  fun id -> vernac_tactic(s,[IDENTIFIER id])
+      
+let hide_string_tactic s tac =
+  let tacfun = (function [QUOTED_STRING str] -> tac str | _ -> assert false) in
+  add_tactic s tacfun;
+  fun str -> vernac_tactic(s,[QUOTED_STRING str])
+
+let hide_identl_tactic s tac =
+  let tacfun = (function [CLAUSE idl] -> tac idl | _ -> assert false) in 
+  add_tactic s tacfun;
+  fun idl -> vernac_tactic(s,[CLAUSE idl])
+
+let hide_constrl_tactic s tac = 
+  let tacfun = function 
+    | ((COMMAND com)::_) as al -> 
+      	tactic_com_list tac 
+          (List.map (function (COMMAND com) -> com | _ -> assert false) al)
+    | ((CONSTR com)::_) as al ->
+      	tac (List.map (function (CONSTR c) -> c | _ -> assert false) al)
+    | _ -> anomaly "hide_constrl_tactic : neither CONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  fun ids -> vernac_tactic(s,(List.map (fun id -> CONSTR id) ids))
+
+let hide_bindl_tactic s tac = 
+  let tacfun = function  
+    | [(BINDINGS  al)] -> tactic_bind_list tac al
+    | [(CBINDINGS al)] -> tac al
+    | _ -> anomaly "hide_bindl_tactic : neither BINDINGS nor CBINDINGS"
+  in 
+  add_tactic s tacfun;
+  fun bindl -> vernac_tactic(s,[(CBINDINGS bindl)])
+      
+let hide_cbindl_tactic s tac = 
+  let tacfun = function 
+    | [(COMMAND com);(BINDINGS al)] -> tactic_com_bind_list tac (com,al)
+    | [(CONSTR  c);(CBINDINGS al)]  -> tac (c,al)
+    | _ -> anomaly "hide_cbindl_tactic : neither CONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  fun (c,bindl) -> vernac_tactic(s,[(CONSTR c);(CBINDINGS bindl)])
+      
+let hide_cbindll_tactic s tac = 
+  let rec getcombinds = function 
+    | ((COMMAND com)::(BINDINGS al)::l) -> (com,al)::(getcombinds l)
+    | []                                ->  [] 
+    | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
+  in  
+  let rec getconstrbinds = function
+    | ((CONSTR c)::(CBINDINGS al)::l) -> (c,al)::(getconstrbinds l)
+    |  []                             ->  [] 
+    | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
+  in  
+  let rec putconstrbinds = function 
+    | (c,binds)::l -> (CONSTR c)::(CBINDINGS binds)::(putconstrbinds l)
+    |  []          -> [] 
+  in
+  let tacfun = function 
+    | ((COMMAND com)::_) as args -> 
+      	tactic_com_bind_list_list tac (getcombinds args)
+    | ((CONSTR com)::_) as args -> tac (getconstrbinds args)
+    | _ -> anomaly "hide_cbindll_tactic : neither CONSTR nor COMMAND"
+  in 
+  add_tactic s tacfun;
+  fun l -> vernac_tactic(s,putconstrbinds l)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
new file mode 100644
index 0000000000..1d03b5c938
--- /dev/null
+++ b/proofs/tacmach.mli
@@ -0,0 +1,219 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+open Environ
+open Reduction
+open Proof_trees
+open Refiner
+open Evar_refiner
+open Tacred
+(*i*)
+
+(* Operations for handling terms under a local typing context. *)
+
+type 'a sigma
+
+val sig_it  : 'a sigma   -> 'a
+val sig_sig : goal sigma -> global_constraints
+val project : goal sigma -> evar_declarations
+
+val re_sig : 'a -> global_constraints -> 'a sigma
+
+val unpackage : 'a sigma -> global_constraints ref * 'a
+val repackage : global_constraints ref -> 'a -> 'a sigma
+val apply_sig_tac :
+  global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+
+val pf_env                : goal sigma -> unsafe_env
+val pf_untyped_hyps       : goal sigma -> constr signature
+val pf_concl              : goal sigma -> constr
+val pf_nth_hyp            : goal sigma -> int -> identifier * constr
+val pf_ctxt               : goal sigma -> ctxtty
+val pf_global             : goal sigma -> identifier -> constr
+val pf_parse_const        : goal sigma -> string -> constr
+val pf_type_of            : goal sigma -> constr -> constr
+val pf_check_type         : goal sigma -> constr -> constr -> constr
+val pf_fexecute           : goal sigma -> constr -> unsafe_judgment
+val hnf_type_of           : goal sigma -> constr -> constr
+
+val pf_get_hyp             : goal sigma -> identifier -> constr
+
+val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
+
+val pf_reduce : (evar_declarations -> constr -> constr) 
+                -> goal sigma -> constr -> constr
+
+val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
+val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function
+val pf_hnf_constr              : goal sigma -> constr -> constr
+val pf_red_product             : goal sigma -> constr -> constr
+val pf_nf                      : goal sigma -> constr -> constr
+val pf_one_step_reduce         : goal sigma -> constr -> constr
+val pf_reduce_to_mind : goal sigma -> constr -> constr * constr * constr
+val pf_reduce_to_ind  : goal sigma  -> constr -> section_path * constr * constr
+val pf_compute        : goal sigma -> constr -> constr
+val pf_unfoldn        : (int list * section_path) list -> goal sigma 
+                        -> constr -> constr
+
+val pf_const_value : goal sigma -> constr -> constr
+val pf_conv_x      : goal sigma -> constr -> constr -> bool
+val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
+
+type validation            = proof_tree list -> proof_tree
+type tactic                = goal sigma -> (goal list sigma * validation)
+type transformation_tactic = proof_tree -> (goal list * validation)
+
+val frontier : transformation_tactic
+
+
+(*s Functions for handling the state of the proof editor. *)
+
+type pftreestate
+
+val proof_of_pftreestate    : pftreestate -> proof_tree
+val cursor_of_pftreestate   : pftreestate -> int list
+val is_top_pftreestate      : pftreestate -> bool
+val evc_of_pftreestate      : pftreestate -> global_constraints
+val top_goal_of_pftreestate : pftreestate -> goal sigma
+val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
+val traverse                : int -> pftreestate -> pftreestate
+val weak_undo_pftreestate   : pftreestate -> pftreestate
+val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
+val solve_pftreestate       : tactic -> pftreestate -> pftreestate
+val mk_pftreestate          : goal -> pftreestate
+val extract_pftreestate     : pftreestate -> constr
+val first_unproven          : pftreestate -> pftreestate
+val last_unproven           : pftreestate -> pftreestate
+val nth_unproven            : int -> pftreestate -> pftreestate
+val node_prev_unproven      : int -> pftreestate -> pftreestate
+val node_next_unproven      : int -> pftreestate -> pftreestate
+val next_unproven           : pftreestate -> pftreestate
+val prev_unproven           : pftreestate -> pftreestate
+val top_of_tree             : pftreestate -> pftreestate
+val change_constraints_pftreestate :
+  global_constraints -> pftreestate -> pftreestate
+
+
+(*s Tacticals re-exported from the Refiner module. *)
+
+val tclIDTAC         : tactic
+val tclORELSE        : tactic -> tactic -> tactic
+val tclTHEN          : tactic -> tactic -> tactic
+val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
+val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENS         : tactic -> tactic list -> tactic
+val tclTHENSI        : tactic -> tactic list -> tactic
+val tclREPEAT        : tactic -> tactic
+val tclFIRST         : tactic list -> tactic
+val tclSOLVE         : tactic list -> tactic
+val tclTRY           : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+val tclCOMPLETE      : tactic -> tactic
+val tclAT_LEAST_ONCE : tactic -> tactic
+val tclFAIL          : tactic
+val tclDO            : int -> tactic -> tactic
+val tclPROGRESS      : tactic -> tactic
+val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+val tclINFO          : tactic -> tactic
+
+val unTAC         : tactic -> goal sigma -> proof_tree sigma
+val vernac_tactic : tactic_expression -> tactic
+val context       : ctxtty -> tactic
+
+
+(*s The most primitive tactics. *)
+
+val refiner         : rule -> tactic
+val introduction    : identifier -> tactic
+val intro_replacing : identifier -> tactic
+val refine          : constr -> tactic
+val convert_concl   : constr -> tactic
+val convert_hyp     : identifier -> constr -> tactic
+val thin            : identifier list -> tactic
+val move_hyp        : bool -> identifier -> identifier -> tactic
+val mutual_fix      : identifier list -> int list -> constr list -> tactic
+val mutual_cofix    : identifier list -> constr list -> tactic
+val rename_bound_var_goal : tactic
+
+
+(*s Tactics handling a list of goals. *)
+
+type validation_list = proof_tree list -> proof_tree list
+
+type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
+
+val first_goal         : 'a list sigma -> 'a sigma
+val goal_goal_list     : 'a sigma -> 'a list sigma
+val apply_tac_list     : tactic -> tactic_list
+val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
+val tactic_list_tactic : tactic_list -> tactic
+val tclFIRSTLIST       : tactic_list list -> tactic_list
+val tclIDTAC_list      : tactic_list
+
+
+(*s Walking constraints re-exported. *)
+
+type walking_constraints = Evar_refiner.walking_constraints
+
+type 'a result_w_tactic  = walking_constraints -> walking_constraints * 'a
+type w_tactic            = walking_constraints -> walking_constraints
+
+val startWalk : 
+  goal sigma -> walking_constraints * (walking_constraints -> tactic)
+
+val walking_THEN        : 'a result_w_tactic -> ('a -> tactic) -> tactic
+val walking             : w_tactic -> tactic
+val w_Focusing_THEN     : section_path -> 'a result_w_tactic 
+                          -> ('a -> w_tactic) -> w_tactic
+val w_Declare           : section_path -> constr -> w_tactic
+val w_Declare_At        : section_path -> section_path -> constr -> w_tactic
+val w_Define            : section_path -> constr -> w_tactic
+val w_Underlying        : walking_constraints -> evar_declarations
+val w_hyps              : walking_constraints -> context
+val w_type_of           : walking_constraints -> constr -> constr
+val w_add_sign          : (identifier * typed_type) 
+                          -> walking_constraints -> walking_constraints
+val w_IDTAC             : w_tactic
+val w_ORELSE            : w_tactic -> w_tactic -> w_tactic
+val ctxt_type_of        : readable_constraints -> constr -> constr
+val w_whd_betadeltaiota : walking_constraints -> constr -> constr
+val w_hnf_constr        : walking_constraints -> constr -> constr
+val w_conv_x            : walking_constraints -> constr -> constr -> bool
+val w_const_value       : walking_constraints -> constr -> constr
+val w_defined_const     : walking_constraints -> constr -> bool
+
+
+(*s Tactic Registration. *)
+
+val add_tactic         : string -> (tactic_arg list -> tactic) -> unit
+val overwriting_tactic : string -> (tactic_arg list -> tactic) -> unit
+
+
+(*s Hiding the implementation of tactics. *)
+
+val hide_tactic  : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+val overwrite_hidden_tactic : 
+  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
+
+
+type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
+
+val hide_atomic_tactic  : string -> tactic -> tactic
+val hide_constr_tactic  : constr hide_combinator
+val hide_constrl_tactic : (constr list) hide_combinator
+val hide_numarg_tactic  : int hide_combinator
+val hide_ident_tactic   : identifier hide_combinator
+val hide_identl_tactic  : (identifier list) hide_combinator
+val hide_string_tactic  : string hide_combinator
+val hide_bindl_tactic   : ((bindOcc * constr) list) hide_combinator
+val hide_cbindl_tactic  : (constr * (bindOcc * constr) list) hide_combinator
+val hide_cbindll_tactic : 
+  ((constr * (bindOcc * constr) list) list) hide_combinator
+
diff --git a/proofs/tacred.ml b/proofs/tacred.ml
new file mode 100644
index 0000000000..a532e8cbcc
--- /dev/null
+++ b/proofs/tacred.ml
@@ -0,0 +1,198 @@
+
+(* $Id$ *)
+
+let is_elim env sigma c =
+  let (sp, cl) = destConst c in
+  if (evaluable_constant env c) && (defined_constant env c) then begin
+    let cb = lookup_constant sp env in 
+    (match cb.cONSTEVAL with
+       | Some _ -> ()
+       | None -> 
+	   (match cb.cONSTBODY with
+	      | Some{contents=COOKED b} ->
+		  cb.cONSTEVAL <- Some(compute_consteval b)
+	      | Some{contents=RECIPE _} ->
+		  anomalylabstrm "Reduction.is_elim"
+		    [< 'sTR"Found an uncooked transparent constant,"; 'sPC ;
+		       'sTR"which is supposed to be impossible" >]
+	      | _ -> assert false));
+    (match (cb.cONSTEVAL) with
+       | Some (Some x) -> x
+       | Some None -> raise Elimconst
+       | _ -> assert false)
+  end else 
+    raise Elimconst
+
+let make_elim_fun sigma f largs =
+  try 
+    let (lv,n,b) = is_elim sigma f 
+    and ll = List.length largs in 
+    if ll < n then raise Redelimination;
+    if b then
+      let labs,_ = chop_list n largs in
+      let p = List.length lv in
+      let la' = map_i (fun q aq ->
+			 try (Rel (p+1-(index (n+1-q) (List.map fst lv)))) 
+			 with Failure _ -> aq) 1
+                  (List.map (lift p) labs) 
+      in
+      it_list_i (fun i c (k,a) -> 
+                   DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
+                   	DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
+    else 
+      f
+  with Elimconst | Failure _ -> 
+    raise Redelimination
+
+let rec red_elim_const env sigma k largs =
+  if not (evaluable_constant env k) then raise Redelimination;
+  let f = make_elim_fun sigma k largs in
+  match whd_betadeltaeta_stack sigma (const_value sigma k) largs with
+    | (DOPN(MutCase _,_) as mc,lrest) ->
+        let (ci,p,c,lf) = destCase mc in
+        (special_red_case sigma (construct_const sigma) p c ci lf, lrest)
+    | (DOPN(Fix _,_) as fix,lrest) -> 
+        let (b,(c,rest)) = 
+	  reduce_fix_use_function f (construct_const sigma) fix lrest
+        in 
+	if b then (nf_beta c, rest) else raise Redelimination
+    | _ -> assert false
+
+and construct_const sigma c stack = 
+  let rec hnfstack x stack =
+    match x with
+      | (DOPN(Const _,_)) as k  ->
+          (try
+             let (c',lrest) = red_elim_const sigma k stack in hnfstack c' lrest
+           with Redelimination ->
+             if evaluable_const sigma k then 
+	       let cval = const_value sigma k in
+	       (match cval with
+                  | DOPN (CoFix _,_) -> (k,stack)
+                  | _                -> hnfstack cval stack) 
+             else 
+	       raise Redelimination)
+      | (DOPN(Abst _,_) as a) ->
+          if evaluable_abst a then 
+	    hnfstack (abst_value a) stack
+          else 
+	    raise Redelimination
+      | DOP2(Cast,c,_)   -> hnfstack c stack
+      | DOPN(AppL,cl)    -> hnfstack (hd_vect cl) (app_tl_vect cl stack)
+      | DOP2(Lambda,_,DLAM(_,c)) ->
+          (match stack with 
+             | [] -> assert false
+             | c'::rest -> stacklam hnfstack [c'] c rest)
+    | DOPN(MutCase _,_) as c_0 ->
+        let (ci,p,c,lf) = destCase c_0 in
+        hnfstack (special_red_case sigma (construct_const sigma) p c ci lf) 
+	  stack
+    | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
+    | DOPN(CoFix _,_) as c_0 -> c_0,stack
+    | DOPN(Fix (_) ,_) as fix -> 
+        let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
+	if reduced then hnfstack fix stack' else raise Redelimination
+    | _ -> raise Redelimination
+  in 
+  hnfstack c stack
+
+(* Hnf reduction tactic: *)
+
+let hnf_constr sigma c = 
+  let rec redrec x largs =
+    match x with
+      | DOP2(Lambda,t,DLAM(n,c)) ->
+          (match largs with
+             | []      -> applist(x,largs)
+             | a::rest -> stacklam redrec [a] c rest)
+      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
+      | DOPN(Const _,_) ->
+          (try
+             let (c',lrest) = red_elim_const sigma x largs in 
+	     redrec c' lrest
+           with Redelimination ->
+             if evaluable_const sigma x then
+               let c = const_value sigma x in
+	       (match c with 
+                  | DOPN(CoFix _,_) -> applist(x,largs)
+		  | _ ->  redrec c largs)
+             else 
+	       applist(x,largs))
+      | DOPN(Abst _,_) ->
+          if evaluable_abst x then 
+	    redrec (abst_value x) largs
+          else 
+	    applist(x,largs)
+      | DOP2(Cast,c,_) -> redrec c largs
+      | DOPN(MutCase _,_) ->
+          let (ci,p,c,lf) = destCase x in
+          (try
+             redrec (special_red_case sigma (whd_betadeltaiota_stack sigma) 
+		       p c ci lf) largs
+           with Redelimination -> 
+	     applist(x,largs))
+      | (DOPN(Fix _,_)) ->
+          let (reduced,(fix,stack)) = 
+            reduce_fix (whd_betadeltaiota_stack sigma) x largs
+          in 
+	  if reduced then redrec fix stack else applist(x,largs)
+      | _         -> applist(x,largs)
+  in 
+  redrec c []
+
+(* Simpl reduction tactic: same as simplify, but also reduces
+   elimination constants *)
+
+let whd_nf sigma c = 
+  let rec nf_app c stack =
+    match c with
+      | DOP2(Lambda,c1,DLAM(name,c2))    ->
+          (match stack with
+             | [] -> (c,[])
+             | a1::rest -> stacklam nf_app [a1] c2 rest)
+      | DOPN(AppL,cl) -> nf_app (hd_vect cl) (app_tl_vect cl stack)
+      | DOP2(Cast,c,_) -> nf_app c stack
+      | DOPN(Const _,_) ->
+          (try
+             let (c',lrest) = red_elim_const sigma c stack in 
+	     nf_app c' lrest
+           with Redelimination -> 
+	     (c,stack))
+      | DOPN(MutCase _,_) ->
+          let (ci,p,d,lf) = destCase c in
+          (try
+             nf_app (special_red_case sigma nf_app p d ci lf) stack
+           with Redelimination -> 
+	     (c,stack))
+      | DOPN(Fix _,_) ->
+          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in 
+	  if reduced then nf_app fix rest else (fix,stack)
+      | _ -> (c,stack)
+  in 
+  applist (nf_app c [])
+
+let nf sigma c = strong (whd_nf sigma) c
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr =
+  | Red
+  | Hnf
+  | Simpl
+  | Cbv of flags
+  | Lazy of flags
+  | Unfold of (int list * section_path) list
+  | Fold of constr list
+  | Change of constr
+  | Pattern of (int list * constr * constr) list
+
+let reduction_of_redexp = function
+  | Red -> red_product
+  | Hnf -> hnf_constr
+  | Simpl -> nf
+  | Cbv f -> cbv_norm_flags f
+  | Lazy f -> clos_norm_flags f
+  | Unfold ubinds -> unfoldn ubinds
+  | Fold cl -> fold_commands cl
+  | Change t -> (fun _ _ -> t)
+  | Pattern lp -> (fun _ -> pattern_occs lp)
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
new file mode 100644
index 0000000000..e965816c7b
--- /dev/null
+++ b/proofs/tacred.mli
@@ -0,0 +1,24 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Reduction
+(*i*)
+
+(* Reduction functions associated to tactics. *)
+
+type red_expr =
+  | Red
+  | Hnf
+  | Simpl
+  | Cbv of Closure.flags
+  | Lazy of Closure.flags
+  | Unfold of (int list * section_path) list
+  | Fold of constr list
+  | Change of constr
+  | Pattern of (int list * constr * constr) list
+
+val reduction_of_redexp : red_expr -> 'a reduction_function
+
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
new file mode 100644
index 0000000000..fce0cc299b
--- /dev/null
+++ b/proofs/typing_ev.ml
@@ -0,0 +1,151 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Environ
+open Reduction
+open Type_errors
+open Typeops
+
+let vect_lift = Array.mapi lift
+let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+
+type 'a mach_flags = {
+  fix : bool;
+  nocheck : bool }
+
+(* The typing machine without information, without universes but with
+   existential variables. *)
+
+let rec execute mf env sigma cstr =
+  match kind_of_term cstr with
+    | IsMeta _ ->
+	anomaly "the kernel does not understand metas"
+    | IsEvar _ ->
+	anomaly "the kernel does not understand existential variables"
+	
+    | IsRel n -> 
+	relative env n
+
+    | IsVar id -> 
+	make_judge cstr (snd (lookup_var id env))
+	  
+    | IsAbst _ ->
+        if evaluable_abst env cstr then 
+	  execute mf env sigma (abst_value env cstr)
+        else 
+	  error "Cannot typecheck an unevaluable abstraction"
+	      
+    | IsConst _ ->
+        make_judge cstr (type_of_constant env sigma cstr)
+	  
+    | IsMutInd _ ->
+	make_judge cstr (type_of_inductive env sigma cstr)
+	  
+    | IsMutConstruct _ -> 
+	let (typ,kind) = destCast (type_of_constructor env sigma cstr) in
+        { uj_val = cstr; uj_type = typ; uj_kind = kind }
+	  
+    | IsMutCase (_,p,c,lf) ->
+        let cj = execute mf env sigma c in
+        let pj = execute mf env sigma p in
+        let lfj = execute_array mf env sigma lf in
+        type_of_case env sigma pj cj lfj
+  
+    | IsFix (vn,i,lar,lfi,vdef) ->
+        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
+          error "General Fixpoints not allowed";
+        let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
+        let fix = mkFix vn i larv lfi vdefv in
+        check_fix env sigma Spset.empty fix;
+	make_judge fix larv.(i)
+	  
+    | IsCoFix (i,lar,lfi,vdef) ->
+        let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
+        let cofix = mkCoFix i larv lfi vdefv in
+        check_cofix env sigma Spset.empty cofix;
+	make_judge cofix larv.(i)
+	  
+    | IsSort (Prop c) -> 
+	type_of_prop_or_set c
+
+    | IsSort (Type u) ->
+	let (j,_) = type_of_type u in j
+	  
+    | IsAppL a ->
+	let la = Array.length a in
+	if la = 0 then error_cant_execute CCI env cstr;
+	let hd = a.(0)
+	and tl = Array.to_list (Array.sub a 1 (la - 1)) in
+	let j = execute mf env sigma hd in
+        let jl = execute_list mf env sigma tl in
+	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
+	j
+	    
+    | IsLambda (name,c1,c2) -> 
+        let j = execute mf env sigma c1 in
+        let var = assumption_of_judgment env sigma j in
+	let env1 = push_rel (name,var) env in
+        let j' = execute mf env1 sigma c2 in 
+        let (j,_) = abs_rel env1 sigma name var j' in
+	j
+	  
+    | IsProd (name,c1,c2) ->
+        let j = execute mf env sigma c1 in
+        let var = assumption_of_judgment env sigma j in
+	let env1 = push_rel (name,var) env in
+        let j' = execute mf env1 sigma c2 in
+	let (j,_) = gen_rel env1 sigma name var j' in
+	j
+	  
+    | IsCast (c,t) ->
+        let cj = execute mf env sigma c in
+        let tj = execute mf env sigma t in
+        cast_rel env sigma cj tj
+	  
+      | _ -> error_cant_execute CCI env cstr
+	  
+and execute_fix mf env sigma lar lfi vdef =
+  let larj = execute_array mf env sigma lar in
+  let lara = Array.map (assumption_of_judgment env sigma) larj in
+  let nlara = 
+    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
+  let env1 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+  let vdefj = execute_array mf env1 sigma vdef in
+  let vdefv = Array.map j_val_only vdefj in
+  let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
+  (lara,vdefv)
+
+and execute_array mf env sigma v =
+  let jl = execute_list mf env sigma (Array.to_list v) in
+  Array.of_list jl
+
+and execute_list mf env sigma = function
+  | [] -> 
+      []
+  | c::r -> 
+      let j = execute mf env sigma c in 
+      let jr = execute_list mf env sigma r in
+      j::jr
+
+
+let safe_machine env sigma constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute mf env sigma constr
+
+
+(* Type of a constr *)
+
+let type_of env sigma c = 
+  let j = safe_machine env sigma c in 
+  nf_betaiota env sigma j.uj_type
+
+(* The typed type of a judgment. *)
+
+let execute_type env sigma constr = 
+  let j = safe_machine env sigma constr in
+  assumption_of_judgment env sigma j
diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli
new file mode 100644
index 0000000000..3ebc2088a2
--- /dev/null
+++ b/proofs/typing_ev.mli
@@ -0,0 +1,12 @@
+
+(* $Id$ *)
+
+(*i*)
+open Term
+open Environ
+open Evd
+(*i*)
+
+val type_of : unsafe_env -> 'a evar_map -> constr -> constr
+
+val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type