deplacement des var. ex. dans proofs

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

10 files changed, 603 insertions, 81 deletions

diff --git a/.depend b/.depend
index f91880e20f..e15dacb691 100644
--- a/.depend
+++ b/.depend
@@ -1,12 +1,11 @@
 kernel/abstraction.cmi: kernel/names.cmi kernel/term.cmi 
-kernel/closure.cmi: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/term.cmi 
+kernel/closure.cmi: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/term.cmi 
 kernel/constant.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \
+kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 kernel/generic.cmi: kernel/names.cmi lib/util.cmi 
 kernel/indtypes.cmi: kernel/environ.cmi kernel/inductive.cmi kernel/names.cmi \
     kernel/term.cmi kernel/univ.cmi 
@@ -15,7 +14,7 @@ kernel/inductive.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
 kernel/instantiate.cmi: kernel/environ.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/term.cmi 
 kernel/names.cmi: lib/pp.cmi 
-kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
+kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi \
     kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi 
 kernel/sosub.cmi: kernel/term.cmi 
@@ -24,7 +23,7 @@ kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi 
 kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/term.cmi \
     kernel/univ.cmi 
-kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
@@ -32,7 +31,7 @@ lib/pp.cmi: lib/pp_control.cmi
 lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/term.cmi 
-library/global.cmi: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
     kernel/typing.cmi kernel/univ.cmi 
 library/impargs.cmi: kernel/names.cmi 
@@ -45,8 +44,10 @@ parsing/coqast.cmi: lib/dyn.cmi
 parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi 
 parsing/pcoq.cmi: parsing/coqast.cmi 
+proofs/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 proofs/pfedit.cmi: lib/pp.cmi 
-proofs/proof_trees.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
+proofs/proof_trees.cmi: parsing/coqast.cmi proofs/evd.cmi kernel/names.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 
@@ -64,28 +65,24 @@ kernel/abstraction.cmo: kernel/generic.cmi kernel/names.cmi kernel/sosub.cmi \
     kernel/term.cmi lib/util.cmi kernel/abstraction.cmi 
 kernel/abstraction.cmx: kernel/generic.cmx kernel/names.cmx kernel/sosub.cmx \
     kernel/term.cmx lib/util.cmx kernel/abstraction.cmi 
-kernel/closure.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+kernel/closure.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
     kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/closure.cmi 
-kernel/closure.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+kernel/closure.cmx: kernel/environ.cmx kernel/generic.cmx \
     kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/closure.cmi 
 kernel/constant.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi kernel/constant.cmi 
 kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx kernel/constant.cmi 
-kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \
+kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi \
     kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi lib/system.cmi kernel/term.cmi kernel/univ.cmi \
     lib/util.cmi kernel/environ.cmi 
-kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx kernel/evd.cmx \
+kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx lib/system.cmx kernel/term.cmx kernel/univ.cmx \
     lib/util.cmx kernel/environ.cmi 
-kernel/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
-    kernel/evd.cmi 
-kernel/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
-    kernel/evd.cmi 
 kernel/generic.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi \
     kernel/generic.cmi 
 kernel/generic.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx \
@@ -100,20 +97,20 @@ kernel/inductive.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/inductive.cmi 
 kernel/inductive.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi 
-kernel/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
+kernel/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi \
     kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/instantiate.cmi 
-kernel/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
+kernel/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/instantiate.cmi 
 kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/util.cmi kernel/names.cmi 
 kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/util.cmx kernel/names.cmi 
 kernel/reduction.cmo: kernel/closure.cmi kernel/constant.cmi \
-    kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi \
+    kernel/environ.cmi kernel/generic.cmi kernel/inductive.cmi \
     kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
     kernel/univ.cmi lib/util.cmi kernel/reduction.cmi 
 kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmx \
-    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmx \
+    kernel/environ.cmx kernel/generic.cmx kernel/inductive.cmx \
     kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx kernel/reduction.cmi 
 kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \
@@ -132,16 +129,14 @@ kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmi 
-kernel/typeops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \
-    kernel/term.cmi kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi \
-    kernel/typeops.cmi 
-kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
-    kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \
-    kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \
-    kernel/typeops.cmi 
+kernel/typeops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/generic.cmi \
+    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi kernel/typeops.cmi 
+kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/generic.cmx \
+    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/typeops.cmi 
 kernel/typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/generic.cmi \
     kernel/indtypes.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
     kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
@@ -168,6 +163,8 @@ lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
 lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
 lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
 lib/util.cmo: lib/pp.cmi lib/util.cmi 
@@ -222,10 +219,14 @@ 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/proof_trees.cmo: parsing/coqast.cmi kernel/term.cmi \
-    proofs/proof_trees.cmi 
-proofs/proof_trees.cmx: parsing/coqast.cmx kernel/term.cmx \
-    proofs/proof_trees.cmi 
+proofs/evd.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
+    proofs/evd.cmi 
+proofs/evd.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
+    proofs/evd.cmi 
+proofs/proof_trees.cmo: parsing/coqast.cmi proofs/evd.cmi kernel/names.cmi \
+    kernel/term.cmi proofs/proof_trees.cmi 
+proofs/proof_trees.cmx: parsing/coqast.cmx proofs/evd.cmx kernel/names.cmx \
+    kernel/term.cmx proofs/proof_trees.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 \
@@ -264,13 +265,13 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmx \
     toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacinterp.cmi toplevel/toplevel.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \
-    library/library.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
     toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
-    library/library.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmi \
-    lib/pp.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmi \
+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 
diff --git a/Makefile b/Makefile
index 42784478f1..c8f0a21df4 100644
--- a/Makefile
+++ b/Makefile
@@ -33,10 +33,10 @@ CONFIG=config/coq_config.cmo
 
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
     lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
-    lib/bstack.cmo lib/edit.cmo
+    lib/bstack.cmo lib/edit.cmo lib/stamps.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
-       kernel/sign.cmo kernel/evd.cmo kernel/constant.cmo \
+       kernel/sign.cmo kernel/constant.cmo \
        kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \
        kernel/environ.cmo kernel/instantiate.cmo \
        kernel/closure.cmo kernel/reduction.cmo \
@@ -51,7 +51,7 @@ 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=proofs/evd.cmo proofs/proof_trees.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
@@ -59,7 +59,7 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernac.cmo \
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
 
-CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(TOPLEVEL)
+CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(PARSING) $(TOPLEVEL)
 CMX=$(CMO:.cmo=.cmx)
 
 # Targets
diff --git a/library/global.ml b/library/global.ml
index f7fac03139..6385e932f4 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -19,9 +19,7 @@ let _ =
 
 (* Then we export the functions of [Typing] on that environment. *)
 
-let evar_map () = evar_map !global_env
 let universes () = universes !global_env
-let metamap () = metamap !global_env
 let context () = context !global_env
 
 let push_var idc = global_env := push_var idc !global_env
@@ -36,7 +34,6 @@ let lookup_rel n = lookup_rel n !global_env
 let lookup_constant sp = lookup_constant sp !global_env
 let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
-let lookup_meta n = lookup_meta n !global_env
 
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
diff --git a/library/global.mli b/library/global.mli
index e959c60914..89cc83cbd5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -6,7 +6,6 @@ open Names
 open Univ
 open Term
 open Sign
-open Evd
 open Constant
 open Inductive
 open Environ
@@ -17,11 +16,9 @@ open Typing
    The functions below are the exactly the same as the ones in [Typing],
    operating on that global environment. *)
 
-val env : unit -> unit environment
+val env : unit -> environment
 
-val evar_map : unit -> unit evar_map
 val universes : unit -> universes
-val metamap : unit -> (int * constr) list
 val context : unit -> context
 
 val push_var : identifier * constr -> unit
@@ -36,7 +33,6 @@ val lookup_rel : int -> name * typed_type
 val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : constr -> mind_specif
-val lookup_meta : int -> constr
 
 val export : string -> compiled_env
 val import : compiled_env -> unit
diff --git a/proofs/evd.ml b/proofs/evd.ml
new file mode 100644
index 0000000000..48b2a4b577
--- /dev/null
+++ b/proofs/evd.ml
@@ -0,0 +1,68 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Sign
+
+(* The type of mappings for existential variables *)
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type 'a evar_info = {
+  evar_concl : typed_type;           (* the type of the evar ...          *)
+  evar_hyps  : typed_type signature; (* ... under a certain signature     *)
+  evar_body  : evar_body;            (* its definition                    *) 
+  evar_info  : 'a option }           (* any other necessary information   *)
+
+type 'a evar_map = 'a evar_info Spmap.t
+
+let mt_evd = Spmap.empty
+
+let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc []
+let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc []
+let map evc k = Spmap.find k evc
+let rmv evc k = Spmap.remove k evc
+let remap evc k i = Spmap.add k i evc
+let in_dom evc k = Spmap.mem k evc
+
+let add_with_info evd sp newinfo = 
+  Spmap.add sp newinfo evd
+
+let add_noinfo evd sp sign typ = 
+  let newinfo = 
+    { evar_concl = typ;
+      evar_hyps  = sign;
+      evar_body  = Evar_empty;
+      evar_info  = None}
+  in 
+  Spmap.add sp newinfo evd
+
+let define evd sp body = 
+  let oldinfo = map evd sp in
+  let newinfo =
+    { evar_concl = oldinfo.evar_concl;
+      evar_hyps  = oldinfo.evar_hyps;
+      evar_body  = Evar_defined body;
+      evar_info  = oldinfo.evar_info} 
+  in
+  match oldinfo.evar_body with
+    | Evar_empty -> Spmap.add sp newinfo evd
+    | _ -> anomaly "cannot define an isevar twice"
+
+(* The list of non-instantiated existential declarations *)
+
+let non_instantiated sigma = 
+  let listsp = toList sigma in
+  List.fold_left 
+    (fun l ((sp,evd) as d) -> 
+       if evd.evar_body = Evar_empty then (d::l) else l)
+    [] listsp
+    
+let is_evar sigma sp = in_dom sigma sp
+
+let is_defined sigma sp =
+  let info = map sigma sp in not (info.evar_body = Evar_empty)
diff --git a/proofs/evd.mli b/proofs/evd.mli
new file mode 100644
index 0000000000..8063f42b02
--- /dev/null
+++ b/proofs/evd.mli
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Sign
+(*i*)
+
+(* The type of mappings for existential variables.
+   The keys are section paths and the associated information is a record
+   containing the type of the evar ([concl]), the signature under which 
+   it was introduced ([hyps]), its definition ([body]) and any other 
+   possible information if necessary ([info]).
+*)
+
+type evar_body =
+  | Evar_empty 
+  | Evar_defined of constr
+
+type 'a evar_info = {
+  evar_concl : typed_type;
+  evar_hyps  : typed_type signature;
+  evar_body  : evar_body;
+  evar_info  : 'a option }
+
+type 'a evar_map
+
+val dom    : 'a evar_map -> section_path list
+val map    : 'a evar_map -> section_path -> 'a evar_info
+val rmv    : 'a evar_map -> section_path -> 'a evar_map
+val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val in_dom : 'a evar_map -> section_path -> bool
+val toList : 'a evar_map -> (section_path * 'a evar_info) list
+
+val mt_evd : 'a evar_map
+val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
+val add_noinfo : 
+  'a evar_map -> section_path -> typed_type signature -> typed_type 
+    -> 'a evar_map
+
+val define : 'a evar_map -> section_path -> constr -> 'a evar_map
+
+val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
+val is_evar : 'a evar_map -> section_path -> bool
+
+val is_defined : 'a evar_map -> section_path -> bool
+
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 77e8314d5f..4680607244 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -1,7 +1,11 @@
 
 (* $Id$ *)
 
+open Names
 open Term
+open Sign
+open Evd
+open Stamps
 
 type bindOcc = 
   | Dep of identifier
@@ -11,20 +15,20 @@ type bindOcc =
 type 'a substitution = (bindOcc * 'a) list
 
 type tactic_arg =
-  | COMMAND       of Coqast.t
-  | CONSTR        of constr
-  | IDENTIFIER    of identifier
-  | INTEGER       of int
-  | CLAUSE        of identifier list
-  | BINDINGS      of Coqast.t substitution
-  | CBINDINGS     of constr   substitution 
-  | QUOTED_STRING of string
-  | TACEXP        of Coqast.t
-  | REDEXP        of string * Coqast.t list
-  | FIXEXP        of identifier * int * Coqast.t
-  | COFIXEXP      of identifier * Coqast.t
-  | LETPATTERNS   of int list option * (identifier * int list) list
-  | INTROPATTERN  of intro_pattern
+  | Command       of Coqast.t
+  | Constr        of constr
+  | Identifier    of identifier
+  | Integer       of int
+  | Clause        of identifier list
+  | Bindings      of Coqast.t substitution
+  | Cbindings     of constr   substitution 
+  | Quoted_string of string
+  | Tacexp        of Coqast.t
+  | Redexp        of string * Coqast.t list
+  | Fixexp        of identifier * int * Coqast.t
+  | Cofixexp      of identifier * Coqast.t
+  | Letpatterns   of int list option * (identifier * int list) list
+  | Intropattern  of intro_pattern
 
 and intro_pattern =
   | IdPat   of identifier
@@ -33,3 +37,206 @@ and intro_pattern =
   | ListPat of intro_pattern list  
 
 and tactic_expression = string * tactic_arg list
+
+
+type pf_status = Complete_proof | Incomplete_proof
+
+type prim_rule_name = 
+  | Intro
+  | Intro_after
+  | Intro_replacing
+  | Fix
+  | Cofix
+  | Refine 
+  | Convert_concl
+  | Convert_hyp
+  | Thin
+  | Move of bool
+
+type prim_rule = {
+  name : prim_rule_name;
+  hypspecs : identifier list;
+  newids : identifier list;
+  params : Coqast.t list;
+  terms : constr list }
+
+type local_constraints = Spset.t
+
+type proof_tree = {
+  status : pf_status;
+  goal : goal;
+  ref : (rule * proof_tree list) option; 
+  subproof : proof_tree option }
+
+and goal =  ctxtty evar_info
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expression
+  | Context of ctxtty
+  | Local_constraints of local_constraints
+
+and ctxtty = {
+  pgm    : constr option;
+  mimick : proof_tree option;
+  lc     : local_constraints } 
+
+and evar_declarations = ctxtty evar_map
+
+let is_bind = function
+  | Bindings _ -> true
+  | _ -> false
+
+let lc_toList lc = Spset.elements lc
+
+(* Functions on goals *)
+
+let mkGOAL ctxt sign cl = 
+  { evar_hyps = sign; 
+    evar_concl = cl; 
+    evar_body = Evar_empty; 
+    evar_info = Some ctxt }
+
+(* Functions on the information associated with existential variables  *)
+
+let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }
+
+let get_ctxt ctxt = 
+  match ctxt.evar_info with
+    | Some x -> x
+    | None -> assert false
+
+let get_pgm evd = 
+  match evd.evar_info with
+    | Some x -> x.pgm
+    | None -> assert false
+
+let set_pgm pgm ctxt = { ctxt with pgm = pgm }
+
+let get_mimick evd   = 
+  match evd.evar_info with
+    | Some x -> x.mimick
+    | None -> assert false
+
+let set_mimick mimick ctxt = {mimick = mimick; pgm = ctxt.pgm;lc=ctxt.lc}
+
+let get_lc evd = 
+  match evd.evar_info with
+    | Some x -> x.lc
+    | None -> assert false
+
+(* Functions on proof trees *)
+
+let ref_of_proof pf =
+  match pf.ref with
+    | None -> failwith "rule_of_proof"
+    | Some r -> r
+
+let rule_of_proof pf =
+  let (r,_) = ref_of_proof pf in r
+
+let children_of_proof pf = 
+  let (_,cl) = ref_of_proof pf in cl
+				    
+let goal_of_proof pf = pf.goal
+
+let subproof_of_proof pf =
+  match pf.subproof with
+    | None -> failwith "subproof_of_proof"
+    | Some pf -> pf
+
+let status_of_proof pf = pf.status
+
+let is_complete_proof pf = pf.status = Complete_proof
+
+let is_leaf_proof pf =
+  match pf.ref with
+    | None -> true
+    | Some _ -> false
+
+let is_tactic_proof pf =
+  match pf.subproof with
+    | Some _ -> true
+    | None -> false
+
+
+(*******************************************************************)
+(*            Constraints for existential variables                *)
+(*******************************************************************)
+
+(* A local constraint is just a set of section_paths *)
+
+(* recall : type local_constraints    = Spset.t *)
+
+(* A global constraint is a mappings of existential variables
+   with some extra information for the program and mimick
+   tactics. *)
+
+type global_constraints  = evar_declarations timestamped
+
+(* A readable constraint is a global constraint plus a focus set
+   of existential variables and a signature. *)
+
+type evar_recordty = {
+  focus : local_constraints;
+  sign  : typed_type signature;
+  decls : evar_declarations }
+
+and readable_constraints = evar_recordty timestamped
+
+(* Functions on readable constraints *)
+			     
+let mt_evcty lc gc = 
+  ts_mk { focus = lc; sign = nil_sign; decls = gc }
+
+let evc_of_evds evds gl = 
+  ts_mk { focus = (get_lc gl); sign = gl.evar_hyps ; decls = evds }
+
+let rc_of_gc gc gl = evc_of_evds (ts_it gc) gl
+		       
+let rc_add evc (k,v) = 
+  ts_mod
+    (fun evc -> { focus =(Spset.add k evc.focus);
+                  sign  = evc.sign;
+                  decls = Evd.add_with_info evc.decls k v })
+    evc
+
+let get_hyps  evc = (ts_it evc).sign
+let get_focus evc = (ts_it evc).focus
+let get_decls evc = (ts_it evc).decls
+let get_gc    evc = (ts_mk (ts_it evc).decls)
+let remap evc (k,v) = 
+  ts_mod
+    (fun evc -> { focus = evc.focus;
+                  sign  = evc.sign;
+                  decls = Evd.remap evc.decls k v })
+    evc
+
+let lc_exists f lc = Spset.fold (fun e b -> (f e) or b) lc false
+
+(* MENTIONS SIGMA SP LOC is true exactly when LOC is defined, and SP is
+ * on LOC's access list, or an evar on LOC's access list mentions SP. *)
+
+let rec mentions sigma sp loc =
+  let loc_evd = map (ts_it sigma).decls loc in 
+  match loc_evd.evar_body with 
+    | Evar_defined _ -> (Spset.mem sp (get_lc loc_evd) 
+			 or lc_exists (mentions sigma sp) (get_lc loc_evd))
+    | _ -> false
+
+(* ACCESSIBLE SIGMA SP LOC is true exactly when SP is on LOC's access list,
+ * or there exists a LOC' on LOC's access list such that
+ * MENTIONS SIGMA SP LOC' is true. *)
+
+let rec accessible sigma sp loc =
+  let loc_evd = map (ts_it sigma).decls loc in 
+  lc_exists (fun loc' -> sp = loc' or mentions sigma sp loc') (get_lc loc_evd)
+
+
+(* [ctxt_access sigma sp] is true when SIGMA is accessing a current
+ * accessibility list ACCL, and SP is either on ACCL, or is mentioned
+ * in the body of one of the ACCL. *)
+
+let ctxt_access sigma sp =
+  lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus
+
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 99d94d01e3..38f7aeb8ec 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -4,8 +4,12 @@
 (*i*)
 open Names
 open Term
+open Evd
 (*i*)
 
+(* This module declares the structure of proof trees, global and
+   readable constraints, and a few utilities on these types *)
+
 type bindOcc = 
   | Dep of identifier
   | NoDep of int
@@ -14,20 +18,20 @@ type bindOcc =
 type 'a substitution = (bindOcc * 'a) list
 
 type tactic_arg =
-  | COMMAND       of Coqast.t
-  | CONSTR        of constr
-  | IDENTIFIER    of identifier
-  | INTEGER       of int
-  | CLAUSE        of identifier list
-  | BINDINGS      of Coqast.t substitution
-  | CBINDINGS     of constr   substitution 
-  | QUOTED_STRING of string
-  | TACEXP        of Coqast.t
-  | REDEXP        of string * Coqast.t list
-  | FIXEXP        of identifier * int * Coqast.t
-  | COFIXEXP      of identifier * Coqast.t
-  | LETPATTERNS   of int list option * (identifier * int list) list
-  | INTROPATTERN  of intro_pattern
+  | Command       of Coqast.t
+  | Constr        of constr
+  | Identifier    of identifier
+  | Integer       of int
+  | Clause        of identifier list
+  | Bindings      of Coqast.t substitution
+  | Cbindings     of constr   substitution 
+  | Quoted_string of string
+  | Tacexp        of Coqast.t
+  | Redexp        of string * Coqast.t list
+  | Fixexp        of identifier * int * Coqast.t
+  | Cofixexp      of identifier * Coqast.t
+  | Letpatterns   of int list option * (identifier * int list) list
+  | Intropattern  of intro_pattern
 
 and intro_pattern =
   | IdPat   of identifier
@@ -36,3 +40,56 @@ and intro_pattern =
   | ListPat of intro_pattern list  
 
 and tactic_expression = string * tactic_arg list
+
+
+type pf_status = Complete_proof | Incomplete_proof
+
+type prim_rule_name = 
+  | Intro
+  | Intro_after
+  | Intro_replacing
+  | Fix
+  | Cofix
+  | Refine 
+  | Convert_concl
+  | Convert_hyp
+  | Thin
+  | Move of bool
+
+type prim_rule = {
+  name : prim_rule_name;
+  hypspecs : identifier list;
+  newids : identifier list;
+  params : Coqast.t list;
+  terms : constr list }
+
+type local_constraints = Spset.t
+
+(* [ref] = [None] if the goal has still to be proved, 
+   and [Some (r,l)] if the rule [r] was applied to the goal
+   and gave [l] as subproofs to be completed. 
+
+   [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; 
+   [p] is then the proof that the goal can be proven if the goals
+   in [l] are solved *)
+
+type proof_tree = {
+  status : pf_status;
+  goal : goal;
+  ref : (rule * proof_tree list) option; 
+  subproof : proof_tree option }
+
+and goal =  ctxtty evar_info
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expression
+  | Context of ctxtty
+  | Local_constraints of local_constraints
+
+and ctxtty = {
+  pgm    : constr option;
+  mimick : proof_tree option;
+  lc     : local_constraints } 
+
+and evar_declarations = ctxtty evar_map
diff --git a/proofs/tmp-src b/proofs/tmp-src
new file mode 100644
index 0000000000..eca0119b18
--- /dev/null
+++ b/proofs/tmp-src
@@ -0,0 +1,148 @@
+
+(********* INSTANTIATE ****************************************************)
+
+(* existential_type gives the type of an existential *)
+let existential_type env k = 
+  let (sp,args) = destConst k in
+  let evd = Evd.map (evar_map env) sp in
+  instantiate_constr 
+    (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args)
+
+(* existential_value gives the value of a defined existential *)
+let existential_value env k =
+  let (sp,args) = destConst k in
+  if defined_const env k then
+    let evd = Evd.map (evar_map env) sp in
+    match evd.evar_body with
+      | EVAR_DEFINED c ->
+ 	  instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args)
+      | _ -> anomalylabstrm "termenv__existential_value"
+            [< 'sTR"The existential variable code just registered a" ;
+               'sPC ; 'sTR"grave internal error." >]
+  else 
+    failwith "undefined existential"
+
+
+(******* REDUCTION ********************************************************)
+
+(* Expanding existential variables (trad.ml, progmach.ml) *)
+(* 1- whd_ise fails if an existential is undefined *)
+let rec whd_ise env = function
+  | DOPN(Const sp,_) as k ->
+      if Evd.in_dom (evar_map env) sp then
+        if defined_constant env k then
+          whd_ise env (constant_value env k)
+        else
+          errorlabstrm "whd_ise"
+            [< 'sTR"There is an unknown subterm I cannot solve" >]
+      else 
+	k
+  | DOP2(Cast,c,_) -> whd_ise env c
+  | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
+  | c -> c
+
+
+(* 2- undefined existentials are left unchanged *)
+let rec whd_ise1 env = function
+  | (DOPN(Const sp,_) as k) ->
+      if Evd.in_dom (evar_map env) sp & defined_const env k then
+        whd_ise1 env (constant_value env k)
+      else 
+	k
+  | DOP2(Cast,c,_) -> whd_ise1 env c
+  | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
+  | c -> c
+
+let nf_ise1 env = strong (whd_ise1 env) env
+
+(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
+ * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
+
+let rec whd_ise1_metas env = function
+  | (DOPN(Const sp,_) as k) ->
+      if Evd.in_dom (evar_map env) sp then
+	if defined_const env k then
+      	  whd_ise1_metas env (const_or_ex_value env k)
+	else 
+      	  let m = DOP0(Meta (new_meta())) in
+	  DOP2(Cast,m,const_or_ex_type env k)
+      else
+	k
+  | DOP2(Cast,c,_) -> whd_ise1_metas env c
+  | c -> c
+
+(********************************************************************)
+(*             Special-Purpose Reduction                            *)
+(********************************************************************)
+
+let whd_meta env = function
+  | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u)
+  | x -> x
+	
+(* Try to replace all metas. Does not replace metas in the metas' values
+ * Differs from (strong whd_meta). *)
+let plain_instance env c = 
+  let s = metamap env in
+  let rec irec = function
+    | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u)
+    | DOP1(oper,c)      -> DOP1(oper, irec c)
+    | DOP2(oper,c1,c2)  -> DOP2(oper, irec c1, irec c2)
+    | DOPN(oper,cl)     -> DOPN(oper, Array.map irec cl)
+    | DOPL(oper,cl)     -> DOPL(oper, List.map irec cl)
+    | DLAM(x,c)         -> DLAM(x, irec c)
+    | DLAMV(x,v)        -> DLAMV(x, Array.map irec v)
+    | u                 -> u
+  in 
+  if s = [] then c else irec c
+    
+(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
+let instance env c = 
+  let s = metamap env in
+  if s = [] then c else nf_betaiota env (plain_instance env c)
+
+(************ REDUCTION.MLI **********************************************)
+
+(*s Special-Purpose Reduction Functions *)
+val whd_meta : 'a reduction_function
+val plain_instance : 'a reduction_function
+val instance : 'a reduction_function
+
+val whd_ise : 'a reduction_function
+val whd_ise1 : 'a reduction_function
+val nf_ise1 : 'a reduction_function
+val whd_ise1_metas : 'a reduction_function
+
+(*********** TYPEOPS *****************************************************)
+
+(* Existentials. *)
+
+let type_of_existential env c =
+  let (sp,args) = destConst c in
+  let info = Evd.map (evar_map env) sp in
+  let hyps = info.evar_hyps in
+  check_hyps (basename sp) env hyps;
+  instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+
+(* Constants or existentials. *)
+
+let type_of_constant_or_existential env c =
+  if is_existential c then
+    type_of_existential env c
+  else
+    type_of_constant env c
+
+
+(******** TYPING **********************************************************)
+
+    | IsMeta n ->
+       	let metaty =
+          try lookup_meta n env
+          with Not_found -> error "A variable remains non instanciated" 
+	in
+        (match kind_of_term metaty with
+           | IsCast (typ,kind) -> 
+	       ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0)
+           | _ ->
+	       let (jty,cst) = execute mf env metaty in
+	       let k = whd_betadeltaiotaeta env jty.uj_type in
+	       ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst))
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 5e1c3ca586..7a16930698 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -13,7 +13,7 @@ open Type_errors
 open Typing
 open G_minicoq
 
-let (env : unit environment ref) = ref empty_environment
+let (env : environment ref) = ref empty_environment
 
 let lookup_var id =
   let rec look n = function