module Logic

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

17 files changed, 492 insertions, 418 deletions

diff --git a/.depend b/.depend
index 659a3c9a18..4a71f43915 100644
--- a/.depend
+++ b/.depend
@@ -50,8 +50,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/logic.cmi: kernel/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \
-    kernel/sign.cmi kernel/term.cmi 
+proofs/logic.cmi: kernel/environ.cmi proofs/proof_trees.cmi kernel/sign.cmi \
+    kernel/term.cmi 
 proofs/pfedit.cmi: lib/pp.cmi 
 proofs/proof_trees.cmi: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
     kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi 
@@ -108,20 +108,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/instantiate.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.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/instantiate.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.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/generic.cmi kernel/inductive.cmi \
+    kernel/environ.cmi kernel/evd.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/generic.cmx kernel/inductive.cmx \
+    kernel/environ.cmx kernel/evd.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 \
@@ -180,13 +180,15 @@ 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 
 lib/util.cmx: lib/pp.cmx lib/util.cmi 
-library/declare.cmo: kernel/constant.cmi library/global.cmi \
-    library/impargs.cmi kernel/inductive.cmi library/lib.cmi \
-    library/libobject.cmi kernel/names.cmi library/nametab.cmi lib/util.cmi \
+library/declare.cmo: kernel/constant.cmi kernel/generic.cmi \
+    library/global.cmi library/impargs.cmi kernel/inductive.cmi \
+    library/lib.cmi library/libobject.cmi kernel/names.cmi \
+    library/nametab.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi \
     library/declare.cmi 
-library/declare.cmx: kernel/constant.cmx library/global.cmx \
-    library/impargs.cmx kernel/inductive.cmx library/lib.cmx \
-    library/libobject.cmx kernel/names.cmx library/nametab.cmx lib/util.cmx \
+library/declare.cmx: kernel/constant.cmx kernel/generic.cmx \
+    library/global.cmx library/impargs.cmx kernel/inductive.cmx \
+    library/lib.cmx library/libobject.cmx kernel/names.cmx \
+    library/nametab.cmx kernel/sign.cmx kernel/term.cmx lib/util.cmx \
     library/declare.cmi 
 library/global.cmo: library/summary.cmi kernel/typing.cmi library/global.cmi 
 library/global.cmx: library/summary.cmx kernel/typing.cmx library/global.cmi 
@@ -230,12 +232,16 @@ 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/logic.cmo: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
-    lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/term.cmi \
-    kernel/typing.cmi proofs/logic.cmi 
-proofs/logic.cmx: parsing/coqast.cmx kernel/evd.cmx kernel/names.cmx \
-    lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/term.cmx \
-    kernel/typing.cmx proofs/logic.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 
+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 
 proofs/proof_trees.cmo: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \
     kernel/sign.cmi lib/stamps.cmi kernel/term.cmi lib/util.cmi \
     proofs/proof_trees.cmi 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f5de3e4e87..e431c1b374 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -47,6 +47,7 @@ let empty_env = {
 let universes env = env.env_universes
 let context env = env.env_context
 let evar_map env = env.env_evar_map
+let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 
 (* Construction functions. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cf89e6dcf7..684758d1e2 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -24,6 +24,7 @@ val empty_env : unsafe_env
 val universes : unsafe_env -> universes
 val context : unsafe_env -> context
 val evar_map : unsafe_env -> evar_map
+val metamap : unsafe_env -> (int * constr) list
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
 val push_rel : name * typed_type -> unsafe_env -> unsafe_env
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index e1f9356df8..09265c988f 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -7,6 +7,7 @@ open Names
 open Generic
 open Term
 open Sign
+open Evd
 open Constant
 open Inductive
 open Environ
@@ -47,7 +48,7 @@ let constant_value env k =
 	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
       | None -> 
 	  anomalylabstrm "termenv__constant_value"
-	    [< 'sTR "a defined constant as no body." >]
+	    [< 'sTR "a defined constant with no body." >]
   else 
     failwith "opaque"
 
@@ -63,3 +64,22 @@ let mis_lc env mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
     (Array.to_list mis.mis_args)
 
+(* Existentials. *)
+
+let name_of_existential n = id_of_string ("?" ^ string_of_int n)
+
+let existential_type env c =
+  let (n,args) = destEvar c in
+  let info = Evd.map (evar_map env) n in
+  let hyps = info.evar_hyps in
+  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+
+let existential_value env c =
+  let (n,args) = destEvar c in
+  let info = Evd.map (evar_map env) n in
+  let hyps = info.evar_hyps in
+  match info.evar_body with
+    | Evar_defined c -> 
+	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
+    | Evar_empty ->
+	anomaly "a defined existential with no body"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index cc63b9a547..8ea57f0887 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -18,6 +18,9 @@ val instantiate_type :
 val constant_value : unsafe_env -> constr -> constr
 val constant_type : unsafe_env -> constr -> typed_type
 
+val existential_value : unsafe_env -> constr -> constr
+val existential_type : unsafe_env -> constr -> constr
+
 val const_abst_opt_value : unsafe_env -> constr -> constr option
 
 val mis_lc : unsafe_env -> mind_specif -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3d67e57d4e..e3b2d9f09f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -17,8 +17,8 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> constr -> constr
-type 'a stack_reduction_function = 
+type reduction_function = unsafe_env -> constr -> constr
+type stack_reduction_function = 
     unsafe_env -> constr -> constr list -> constr * constr list
 
 (*************************************)
@@ -739,7 +739,7 @@ let pb_equal = function
   | CONV_LEQ -> CONV
   | CONV -> CONV
 
-type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
+type conversion_function = unsafe_env -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
@@ -936,13 +936,40 @@ let is_conv env = test_conversion conv env
 let is_conv_leq env = test_conversion conv_leq env
 
 
+(********************************************************************)
+(*             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 s c = 
+  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 s env c = 
+  if s = [] then c else nf_betaiota env (plain_instance s c)
+
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
  * with an HNF on the first argument to produce a product.
  * if this does not work, then we use the string S as part of our
- * error message.
- *)
+ * error message. *)
+
 let hnf_prod_app env s t n =
   match whd_betadeltaiota env t with
     | DOP2(Prod,_,b) -> sAPP b n
@@ -1304,6 +1331,56 @@ let poly_args env t =
     | _ -> []
 
 
+(* Expanding existential variables (trad.ml, progmach.ml) *)
+(* 1- whd_ise fails if an existential is undefined *)
+let rec whd_ise env = function
+  | DOPN(Evar sp,_) as k ->
+      let evm = evar_map env in
+      if Evd.in_dom evm sp then
+        if Evd.is_defined evm sp 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(Evar sp,_) as k) ->
+      let evm = evar_map env in
+      if Evd.in_dom evm sp & Evd.is_defined evm sp then
+        whd_ise1 env (existential_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(Evar n,_) as k) ->
+      let evm = evar_map env in
+      if Evd.in_dom evm n then
+	if Evd.is_defined evm n then
+      	  whd_ise1_metas env (existential_value env k)
+	else 
+      	  let m = DOP0(Meta (new_meta())) in
+	  DOP2(Cast,m,existential_type env k)
+      else
+	k
+  | DOP2(Cast,c,_) -> whd_ise1_metas env c
+  | c -> c
+
+
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
 
 let under_outer_cast f = function
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f24431a2f7..771899fad8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -16,58 +16,58 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> constr -> constr
+type reduction_function = unsafe_env -> constr -> constr
 
-type 'a stack_reduction_function = 
+type stack_reduction_function = 
     unsafe_env -> constr -> constr list -> constr * constr list
 
-val whd_stack : 'a stack_reduction_function
+val whd_stack : stack_reduction_function
 
 (*s Reduction Function Operators *)
-val under_casts : 'a reduction_function -> 'a reduction_function
-val strong : 'a reduction_function -> 'a reduction_function
-val strong_prodspine : 'a reduction_function -> 'a reduction_function
+val under_casts : reduction_function -> reduction_function
+val strong : reduction_function -> reduction_function
+val strong_prodspine : reduction_function -> reduction_function
 val stack_reduction_of_reduction : 
-  'a reduction_function -> 'a stack_reduction_function
+  reduction_function -> stack_reduction_function
 
 (*s Generic Optimized Reduction Functions using Closures *)
 
 (* 1. lazy strategy *)
-val clos_norm_flags : Closure.flags -> 'a reduction_function
+val clos_norm_flags : Closure.flags -> reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
-val nf_beta : 'a reduction_function
-val nf_betaiota : 'a reduction_function
-val nf_betadeltaiota : 'a reduction_function
+val nf_beta : reduction_function
+val nf_betaiota : reduction_function
+val nf_betadeltaiota : reduction_function
 
 (* 2. call by value strategy *)
-val cbv_norm_flags : flags -> 'a reduction_function
-val cbv_beta : 'a reduction_function
-val cbv_betaiota : 'a reduction_function
-val cbv_betadeltaiota : 'a reduction_function
+val cbv_norm_flags : flags -> reduction_function
+val cbv_beta : reduction_function
+val cbv_betaiota : reduction_function
+val cbv_betadeltaiota : reduction_function
 
 (* 3. lazy strategy, weak head reduction *)
-val whd_beta : 'a reduction_function
-val whd_betaiota : 'a reduction_function
-val whd_betadeltaiota : 'a reduction_function
+val whd_beta : reduction_function
+val whd_betaiota : reduction_function
+val whd_betadeltaiota : reduction_function
 
-val whd_beta_stack : 'a stack_reduction_function
-val whd_betaiota_stack : 'a stack_reduction_function
-val whd_betadeltaiota_stack : 'a stack_reduction_function
+val whd_beta_stack : stack_reduction_function
+val whd_betaiota_stack : stack_reduction_function
+val whd_betadeltaiota_stack : stack_reduction_function
 
 
 (*s Head normal forms *)
-val whd_const_stack : section_path list -> 'a stack_reduction_function
-val whd_const : section_path list -> 'a reduction_function
-val whd_delta_stack : 'a stack_reduction_function
-val whd_delta : 'a reduction_function
-val whd_betadelta_stack : 'a stack_reduction_function
-val whd_betadelta : 'a reduction_function
-val whd_betadeltat_stack : 'a stack_reduction_function
-val whd_betadeltat : 'a reduction_function
-val whd_betadeltatiota_stack : 'a stack_reduction_function
-val whd_betadeltatiota : 'a reduction_function
-val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
-val whd_betadeltaiotaeta : 'a reduction_function
+val whd_const_stack : section_path list -> stack_reduction_function
+val whd_const : section_path list -> reduction_function
+val whd_delta_stack : stack_reduction_function
+val whd_delta : reduction_function
+val whd_betadelta_stack : stack_reduction_function
+val whd_betadelta : reduction_function
+val whd_betadeltat_stack : stack_reduction_function
+val whd_betadeltat : reduction_function
+val whd_betadeltatiota_stack : stack_reduction_function
+val whd_betadeltatiota : reduction_function
+val whd_betadeltaiotaeta_stack : stack_reduction_function
+val whd_betadeltaiotaeta : reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
@@ -98,15 +98,15 @@ val is_info_cast_type : unsafe_env -> constr -> bool
 val contents_of_cast_type : unsafe_env -> constr -> contents
 val poly_args : unsafe_env -> constr -> int list
 
-val whd_programs : 'a reduction_function
+val whd_programs : reduction_function
 
 val unfoldn : 
-  (int list * section_path) list -> 'a reduction_function
-val fold_one_com : constr -> 'a reduction_function
-val fold_commands : constr list -> 'a reduction_function
+  (int list * section_path) list -> reduction_function
+val fold_one_com : constr -> reduction_function
+val fold_commands : constr list -> reduction_function
 val subst_term_occ : int list -> constr -> constr -> constr
-val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
-val compute : 'a reduction_function
+val pattern_occs : (int list * constr * constr) list -> reduction_function
+val compute : reduction_function
 
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
@@ -131,32 +131,45 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
 val convert_forall2 : 
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
-type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
+type conversion_function = unsafe_env -> constr -> constr -> constraints
 
-val fconv : conv_pb -> 'a conversion_function
+val fconv : conv_pb -> conversion_function
 
 (* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
    [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
 
-val conv : 'a conversion_function
-val conv_leq : 'a conversion_function
+val conv : conversion_function
+val conv_leq : conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> unsafe_env 
-    -> constr array -> constr array -> constraints
+  conversion_function -> unsafe_env -> constr array 
+    -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> unsafe_env 
+  (int -> conversion_function) -> unsafe_env 
     -> constr array -> constr array -> constraints
 
 val is_conv : unsafe_env -> constr -> constr -> bool
 val is_conv_leq : unsafe_env -> constr -> constr -> bool
 
+
+(*s Special-Purpose Reduction Functions *)
+
+val whd_meta : reduction_function
+val plain_instance : (int * constr) list -> constr -> constr
+val instance : (int * constr) list -> reduction_function
+
+val whd_ise : reduction_function
+val whd_ise1 : reduction_function
+val nf_ise1 : reduction_function
+val whd_ise1_metas : reduction_function
+
+
 (*s Obsolete Reduction Functions *)
 
 val hnf : unsafe_env -> constr -> constr * constr list
-val apprec : 'a stack_reduction_function
-val red_product : 'a reduction_function
+val apprec : stack_reduction_function
+val red_product : reduction_function
 val find_mrectype : unsafe_env -> constr -> constr * constr list
 val find_minductype : unsafe_env -> constr -> constr * constr list
 val find_mcoinductype : unsafe_env -> constr -> constr * constr list
diff --git a/kernel/term.ml b/kernel/term.ml
index a1232ab5a9..5d9817fdef 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -353,7 +353,7 @@ let hd_app  = function
 
 (* Destructs a constant *)
 let destConst = function
-  | DOPN (Const  sp, a) -> (sp, a)
+  | DOPN (Const sp, a) -> (sp, a)
   | _ -> invalid_arg "destConst"
 
 let path_of_const = function
@@ -364,6 +364,11 @@ let args_of_const = function
   | DOPN (Const _,args) -> args
   | _ -> anomaly "args_of_const called with bad args"
 
+(* Destructs an existential variable *)
+let destEvar = function
+  | DOPN (Evar n, a) -> (n,a)
+  | _ -> invalid_arg "destEvar"
+
 (* Destructs an abstract term *)
 let destAbst = function
   | DOPN (Abst sp, a) -> (sp, a)
diff --git a/kernel/term.mli b/kernel/term.mli
index 8e16e8fbc3..1fa03507fd 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -272,6 +272,9 @@ val destConst : constr -> section_path * constr array
 val path_of_const : constr -> section_path
 val args_of_const : constr -> constr array
 
+(* Destructs an existential variable *)
+val destEvar : constr -> int * constr array
+
 (* Destrucy an abstract term *)
 val destAbst : constr -> section_path * constr array
 val path_of_abst : constr -> section_path
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a95b54b66e..0a4419a608 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -33,6 +33,10 @@ val type_of_constructor : unsafe_env -> constr -> constr
 val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment 
   -> unsafe_judgment array -> unsafe_judgment
 
+val type_case_branches :
+  unsafe_env -> constr -> constr -> constr -> constr 
+    -> constr * constr array * constr 
+
 val type_of_prop_or_set : contents -> unsafe_judgment
 
 val type_of_type : universe -> unsafe_judgment * constraints
diff --git a/library/declare.ml b/library/declare.ml
index 60a1c5960d..cb5ec1b40d 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -3,6 +3,9 @@
 
 open Util
 open Names
+open Generic
+open Term
+open Sign
 open Constant
 open Inductive
 open Libobject
@@ -126,3 +129,42 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
+
+(* Global references. *)
+
+let first f v =
+  let n = Array.length v in
+  let rec look_for i =
+    if i = n then raise Not_found;
+    try f i v.(i) with Not_found -> look_for (succ i)
+  in
+  look_for 0
+
+let mind_oper_of_id sp id mib =
+  first 
+    (fun tyi mip ->
+       if id = mip.mind_typename then 
+	 MutInd (sp,tyi)
+       else
+	 first 
+	   (fun cj cid -> 
+	      if id = cid then 
+		MutConstruct((sp,tyi),succ cj) 
+	      else raise Not_found) 
+	   mip.mind_consnames)
+    mib.mind_packets
+
+let global_operator sp id =
+  try
+    let _ = Global.lookup_constant sp in Const sp
+  with Not_found -> 
+    let mib = Global.lookup_mind sp in
+    mind_oper_of_id sp id mib
+
+let global_reference id =
+  let sp = Nametab.sp_of_id CCI id in
+  let oper = global_operator sp id in
+  let hyps = get_globals (Global.context ()) in
+  let ids =  ids_of_sign hyps in
+  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+
diff --git a/library/declare.mli b/library/declare.mli
index 21486c250e..f7a0fa0884 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,3 +23,11 @@ val declare_constant : identifier -> constant_entry -> unit
 
 val declare_mind : mutual_inductive_entry -> unit
 
+
+(*s It also provides a function [global_reference] to construct a global
+  constr (a constant, an inductive or a constructor) from an identifier.
+  To do so, it first looks for the section path using [Nametab.sp_of_id] and
+  then constructs the corresponding term, associated to the current 
+  environment of variables. *)
+
+val global_reference : identifier -> constr
diff --git a/library/global.mli b/library/global.mli
index 89cc83cbd5..2e0a541df2 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -13,7 +13,7 @@ open Typing
 (*i*)
 
 (* This module defines the global environment of Coq. 
-   The functions below are the exactly the same as the ones in [Typing],
+   The functions below are exactly the same as the ones in [Typing],
    operating on that global environment. *)
 
 val env : unit -> environment
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a4578b9216..bf174a59ca 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -2,153 +2,114 @@
 (* $Id$ *)
 
 open Pp
+open Util
 open Names
 open Evd
+open Generic
 open Term
+open Sign
+open Environ
 open Reduction
 open Proof_trees
-open Typing
+open Typeops
 open Coqast
+open Declare
 
-let pr_prim_rule = function
-  | {name=Intro;newids=[id]} -> [< 'sTR"Intro " ; print_id id >]
-
-  | {name=Intro_after;newids=[id]} -> [< 'sTR"Intro after " ; print_id id >]
-
-  | {name=Intro_replacing;newids=[id]} -> 
-      [< 'sTR"Intro replacing " ; print_id id >]
-
-  | {name=Fix;newids=[f];params=[Num(_,n)]} -> 
-         [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n>]
-
-  | {name=Fix;newids=(f::lf);params=(Num(_,n))::ln;terms=lar} -> 
-      let rec print_mut = function 
-	| (f::lf),((Num(_,n))::ln),(ar::lar) -> 
-            [< print_id f; 'sTR"/"; 'iNT n; 'sTR" : "; prterm ar;
-               print_mut (lf,ln,lar)>]
-        | _ -> [<>] 
-      in
-      [< 'sTR"Fix "; print_id f; 'sTR"/"; 'iNT n;
-	 'sTR" with "; print_mut (lf,ln,lar) >]
-
-  | {name=COFIX;newids=[f];terms=[]} -> 
-      [< 'sTR"Cofix "; print_id f >]
-
-  | {name=COFIX;newids=(f::lf);terms=lar} -> 
-      let rec print_mut = function 
-	| (f::lf),(ar::lar) -> 
-	    [< print_id f; 'sTR" : "; prterm ar; print_mut (lf,lar)>]
-        | _ -> [<>] 
-      in
-      [< 'sTR"Cofix "; print_id f;  'sTR" with "; print_mut (lf,lar) >]
-
-  | {name=REFINE;terms=[c]} -> 
-      [< 'sTR(if occur_meta c then "Refine " else "Exact ") ; prterm c >]
-      
-  | {name=CONVERT_CONCL;terms=[c]} ->
-      [< 'sTR"Change " ; prterm c >]
-      
-  | {name=CONVERT_HYP;hypspecs=[id];terms=[c]} ->
-      [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; print_id id >]
-      
-  | {name=THIN;hypspecs=ids} ->
-      [< 'sTR"Clear " ; prlist_with_sep pr_spc print_id ids >]
-      
-  | {name=MOVE withdep;hypspecs=[id1;id2]} ->
-      [< 'sTR (if withdep then "Dependent " else "");
-	 'sTR"Move " ; print_id id1; 'sTR " after "; print_id id2 >]
-      
-  | _ -> anomaly "pr_prim_rule: Unrecognized primitive rule"
-
-let conv_leq_goal sigma arg ty conclty =
-  if not (conv_x_leq sigma ty conclty) then
-    errorlabstrm "Logic.conv_leq_goal"
-      [< 'sTR"refiner was given an argument"; 'bRK(1,1); prterm arg; 'sPC;
-         'sTR"of type"; 'bRK(1,1); prterm ty; 'sPC;
-         'sTR"instead of"; 'bRK(1,1); prterm conclty >]
-
-let rec mkREFGOALS sigma goal goalacc conclty trm =
+type refiner_error =
+  | BadType of constr * constr * constr
+  | OccurMeta of constr
+  | CannotApply of constr * constr
+
+exception RefinerError of refiner_error
+
+let conv_leq_goal env arg ty conclty =
+  if not (is_conv_leq env ty conclty) then 
+    raise (RefinerError (BadType (arg,ty,conclty)))
+
+let type_of env hyps c =
+  failwith "TODO: typage avec VE"
+
+let execute_type env ty =
+  failwith "TODO: typage type avec VE"
+
+let rec mk_refgoals env goal goalacc conclty trm =
+  let hyps = goal.goal_ev.evar_hyps in
   match trm with
     | DOP0(Meta mv) ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
-	let ctxt = outSOME goal.info in 
-	(mkGOAL ctxt goal.hyps (nf_betaiota conclty))::goalacc,conclty
+	let ctxt = goal.goal_ctxtty in 
+	(mk_goal ctxt hyps (nf_betaiota env conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
-	let _ = type_of sigma goal.hyps ty in
-	let _ = conv_leq_goal sigma trm ty conclty in
-	mkREFGOALS sigma goal goalacc ty t
+	let _ = type_of env hyps ty in
+	conv_leq_goal env trm ty conclty;
+	mk_refgoals env goal goalacc ty t
 
     | DOPN(AppL,cl) ->
-	let (acc',hdty) = mkHDGOALS sigma goal goalacc (hd_vect cl) in
+	let (acc',hdty) = mk_hdgoals env goal goalacc (array_hd cl) in
 	let (acc'',conclty') = 
-	  mkARGGOALS sigma goal acc' hdty (list_of_tl_vect cl) in
-	let _ = conv_leq_goal sigma trm conclty' conclty in
+	  mk_arggoals env goal acc' hdty (array_list_of_tl cl) in
+	let _ = conv_leq_goal env trm conclty' conclty in
         (acc'',conclty')
 
     | DOPN(MutCase _,_) as mc -> 
 	let (_,p,c,lf) = destCase mc in
-	let (acc',lbrty,conclty') = mkCASEGOALS sigma goal goalacc p c in
+	let (acc',lbrty,conclty') = mk_casegoals env goal goalacc p c in
 	let acc'' = 
-	  it_vect2
-            (fun lacc ty fi -> fst (mkREFGOALS sigma goal lacc ty fi))
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals env goal lacc ty fi))
             acc' lbrty lf 
 	in
-	let _ = conv_leq_goal sigma trm conclty' conclty in 
+	let _ = conv_leq_goal env trm conclty' conclty in 
 	(acc'',conclty')
 
     | t -> 
-	if occur_meta t then
-          errorlabstrm "Logic.mkREFGOALS"
-            [< 'sTR"cannot refine with term"; 'bRK(1,1); prterm t;
-               'sPC; 'sTR"because there are metavariables, and it is";
-               'sPC; 'sTR"neither an application nor a Case" >];
-      	let t'ty = type_of sigma goal.hyps t in
-	conv_leq_goal sigma t t'ty conclty;
+	if occur_meta t then raise (RefinerError (OccurMeta t));
+      	let t'ty = type_of env hyps t in
+	conv_leq_goal env t t'ty conclty;
         (goalacc,t'ty)
 
 (* Same as mkREFGOALS but without knowing te type of the term. Therefore,
  * Metas should be casted. *)
 
-and mkHDGOALS sigma goal goalacc = function
-  | DOP2(Cast,DOP0(Meta mv),ty) ->
-      let _ = type_of sigma goal.hyps ty in
-      let ctxt = outSOME goal.info in  
-      (mkGOAL ctxt goal.hyps (nf_betaiota ty))::goalacc,ty
-	
-  | DOPN(AppL,cl) ->
-      let (acc',hdty) = mkHDGOALS sigma goal goalacc (hd_vect cl) in
-      mkARGGOALS sigma goal acc' hdty (list_of_tl_vect cl)
+and mk_hdgoals env goal goalacc trm =
+  let hyps = goal.goal_ev.evar_hyps in
+  match trm with
+    | DOP2(Cast,DOP0(Meta mv),ty) ->
+	let _ = type_of env hyps ty in
+	let ctxt = goal.goal_ctxtty in  
+	(mk_goal ctxt hyps (nf_betaiota env ty))::goalacc,ty
+	  
+    | DOPN(AppL,cl) ->
+	let (acc',hdty) = mk_hdgoals env goal goalacc (array_hd cl) in
+	mk_arggoals env goal acc' hdty (array_list_of_tl cl)
 	
-  | DOPN(MutCase _,_) as mc -> 
-      let (_,p,c,lf) = destCase mc in
-      let (acc',lbrty,conclty') = mkCASEGOALS sigma goal goalacc p c in
-      let acc'' = it_vect2 
-                    (fun lacc ty fi -> fst (mkREFGOALS sigma goal lacc ty fi))
-                    acc' lbrty lf in
-      (acc'',conclty')
+    | DOPN(MutCase _,_) as mc -> 
+	let (_,p,c,lf) = destCase mc in
+	let (acc',lbrty,conclty') = mk_casegoals env goal goalacc p c in
+	let acc'' = 
+	  array_fold_left2
+            (fun lacc ty fi -> fst (mk_refgoals env goal lacc ty fi))
+            acc' lbrty lf 
+	in
+	(acc'',conclty')
 
-  | t -> goalacc,type_of sigma goal.hyps t
+    | t -> goalacc,type_of env hyps t
 
-and mkARGGOALS sigma goal goalacc funty = function
+and mk_arggoals env goal goalacc funty = function
   | [] -> goalacc,funty
   | harg::tlargs ->
-      (match whd_betadeltaiota sigma funty with
+      (match whd_betadeltaiota env funty with
 	 | DOP2(Prod,c1,b) ->
-	     let (acc',hargty) = mkREFGOALS sigma goal goalacc c1 harg in
-	     mkARGGOALS sigma goal acc' (sAPP b harg) tlargs
-	 | t ->
-             errorlabstrm "Logic.mkARGGOALS"
-               [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
-                  prterm t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
-                  prterm harg >])
-
-and mkCASEGOALS sigma goal goalacc p c= 
-  let (acc',ct) = mkHDGOALS sigma goal goalacc c in 
-  let (acc'',pt) = mkHDGOALS sigma goal acc' p in
-  let (_,lbrty,conclty) =
-    type_case_branches (gLOB goal.hyps) sigma ct pt p c in
+	     let (acc',hargty) = mk_refgoals env goal goalacc c1 harg in
+	     mk_arggoals env goal acc' (sAPP b harg) tlargs
+	 | t -> raise (RefinerError (CannotApply (t,harg))))
+
+and mk_casegoals env goal goalacc p c= 
+  let (acc',ct) = mk_hdgoals env goal goalacc c in 
+  let (acc'',pt) = mk_hdgoals env goal acc' p in
+  let (_,lbrty,conclty) = type_case_branches env ct pt p c in
   (acc'',lbrty,conclty)
 
 
@@ -159,18 +120,19 @@ let collect_meta_variables c =
   let rec collrec acc = function
     | DOP0(Meta mv) -> mv::acc
     | DOP2(Cast,c,t) -> collrec acc c
-    | DOPN(AppL,cl) -> it_vect collrec acc cl
-    | DOPN(MutCase _,_) as mc -> let (_,p,c,lf) = destCase mc in
-      it_vect collrec (collrec (collrec acc p) c) lf
+    | DOPN(AppL,cl) -> Array.fold_left collrec acc cl
+    | DOPN(MutCase _,_) as mc -> 
+	let (_,p,c,lf) = destCase mc in
+	Array.fold_left collrec (collrec (collrec acc p) c) lf
     | _ -> acc
   in 
   List.rev(collrec [] c)
 
 let new_meta_variables = 
   let rec newrec = function
-    | DOP0(Meta mv) -> DOP0(Meta (newMETA()))
-    | DOP2(Cast,c,t) -> DOP2(Cast,newrec c,t)
-    | DOPN(AppL,cl) -> DOPN(AppL,Array.map newrec cl)
+    | DOP0(Meta _) -> DOP0(Meta (new_meta()))
+    | DOP2(Cast,c,t) -> DOP2(Cast, newrec c, t)
+    | DOPN(AppL,cl) -> DOPN(AppL, Array.map newrec cl)
     | DOPN(MutCase _,_) as mc ->
         let (ci,p,c,lf) = destCase mc in
         mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf)
@@ -178,7 +140,7 @@ let new_meta_variables =
   in 
   newrec
 
-let mk_assumption sigma sign c = fexecute_type sigma sign c
+let mk_assumption env c = execute_type env c
 				   
 let sign_before id = 
   let rec aux = function
@@ -247,21 +209,24 @@ let move_after with_dep toleft (left,htfrom,right) hto =
     
 (* Primitive tactics are handled here *)
 
-let prim_refiner r sigma goal =
-  match r, goal with
-    | {name=INTRO;newids=[id]}, {hyps=sign;concl=cl;info=(Some info)} ->
+let prim_refiner r env goal =
+  let ev = goal.goal_ev in
+  let sign = ev.evar_hyps in
+  let cl = ev.evar_concl in
+  let info = goal.goal_ctxtty in
+  match r with
+    | { name = Intro; newids = [id] } ->
     	if mem_sign sign id then error "New variable is already declared";
         (match strip_outer_cast cl with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
-	       let a = mk_assumption sigma sign c1
+	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mkGOAL info (add_sign (id,a) sign) (sAPP b v) in 
+	       let sg = mk_goal info (add_sign (id,a) sign) (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
-    | {name=INTRO_AFTER;newids=[id];hypspecs=[whereid]}, 
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
     	if mem_sign sign id then error "New variable is already declared";
         (match strip_outer_cast cl with
 	   | DOP2(Prod,c1,b) ->
@@ -271,15 +236,14 @@ let prim_refiner r sigma goal =
                          (global_vars c1)) then
 		 error 
 		   "Can't introduce at that location: free variable conflict";
-	       let a = mk_assumption sigma sign c1
+	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mkGOAL info 
+	       let sg = mk_goal info 
 			  (add_sign_after whereid (id,a) sign) (sAPP b v) in 
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
-    | {name=INTRO_REPLACING;newids=[];hypspecs=[id]},
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Intro_replacing; newids = []; hypspecs = [id] } ->
 	(match strip_outer_cast cl with
            | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
@@ -291,21 +255,21 @@ let prim_refiner r sigma goal =
 	       then 
 		 error 
 		   "Can't introduce at that location: free variable conflict";
-	       let a = mk_assumption sigma sign c1
+	       let a = mk_assumption env sign c1
 	       and v = VAR id in
-	       let sg = mkGOAL info (add_sign_replacing id (id,a) sign) 
+	       let sg = mk_goal info (add_sign_replacing id (id,a) sign) 
 			  (sAPP b v) in
 	       [sg]
 	   | _ -> error "Introduction needs a product")
 	
-    | {name=FIX;hypspecs=[];terms=[];newids=[f];params=[Num(_,n)]},
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Fix; hypspecs = []; terms = []; 
+	newids = [f]; params = [Num(_,n)] } ->
      	let rec check_ind k cl = 
           match whd_castapp cl with 
             | DOP2(Prod,c1,DLAM(_,b)) -> 
             	if k = 1 then 
 		  (try 
-		     find_minductype sigma c1 
+		     find_minductype env c1 
 		   with Induc -> 
 		     error "cannot do a fixpoint on a non inductive type")
             	else 
@@ -314,18 +278,17 @@ 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 sigma sign cl in
-        let sg = mkGOAL info (add_sign (f,a) sign) cl in
+        let a = mk_assumption env sign cl in
+        let sg = mk_goal info (add_sign (f,a) sign) cl in
         [sg]
     
-    | {name=FIX;hypspecs=[];terms=lar;newids=lf;params=ln},
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
      	let rec check_ind k cl = 
           match whd_castapp cl with 
             | DOP2(Prod,c1,DLAM(_,b)) -> 
             	if k = 1 then 
 		  (try 
-		     find_minductype sigma c1 
+		     find_minductype env c1 
 		   with Induc -> 
 		     error "cannot do a fixpoint on a non inductive type")
             	else 
@@ -338,64 +301,64 @@ let prim_refiner r sigma goal =
 	  | (ar::lar'),(f::lf'),((Num(_,n))::ln')->
 	      let (sp',_,_)  = destMutInd (fst (check_ind n ar)) in 
 	      if not (sp=sp') then 
-		error "fixpoints should be on the same mutual inductive declaration";
+		error ("fixpoints should be on the same " ^ 
+		       "mutual inductive declaration");
 	      if mem_sign sign f then 
 		error "name already used in the environment";
-	      let a = mk_assumption sigma sign ar in
+	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf',ln')
 	  | ([],[],[]) -> 
-	      List.map (mkGOAL info sign) (cl::lar)
+	      List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
 	in 
 	mk_sign sign (cl::lar,lf,ln)
 
-    | {name=COFIX;hypspecs=[];terms=lar;newids=lf;params=[]},
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Cofix; hypspecs = []; terms = lar; newids = lf; params = [] } ->
      	let rec check_is_coind cl = 
-          match (whd_betadeltaiota sigma (whd_castapp cl)) with 
+          match (whd_betadeltaiota env (whd_castapp cl)) with 
             | DOP2(Prod,c1,DLAM(_,b)) -> check_is_coind  b
             | b  -> 
 		(try 
-		   let _ = find_mcoinductype sigma b in true
+		   let _ = find_mcoinductype env b in true
                  with Induc -> 
-		   error "All methods must construct elements in coinductive types")
+		   error ("All methods must construct elements " ^
+			  "in coinductive types"))
 	in
      	let _ = List.for_all check_is_coind (cl::lar) in
         let rec mk_sign sign = function 
           | (ar::lar'),(f::lf') ->
 	      if mem_sign sign f then 
 		error "name already used in the environment";
-	      let a = mk_assumption sigma sign ar in
+	      let a = mk_assumption env sign ar in
 	      mk_sign (add_sign (f,a) sign) (lar',lf')
-	  | ([],[]) -> List.map (mkGOAL info sign) (cl::lar)
+	  | ([],[]) -> List.map (mk_goal info sign) (cl::lar)
 	  | _ -> error "not the right number of arguments"
      	in 
 	mk_sign sign (cl::lar,lf)
 	  
-    | {name=REFINE;terms=[c]},{hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Refine; terms = [c] } ->
 	let c = new_meta_variables c in
-	let (sgl,cl') = mkREFGOALS sigma goal [] cl c in
+	let (sgl,cl') = mk_refgoals env goal [] cl c in
 	let sgl = List.rev sgl in
 	sgl
 
-    | {name=CONVERT_CONCL;terms=[cl']},{hyps=sign;concl=cl;info=Some info} ->
-    	let cl'ty = type_of sigma sign cl' in
-	if conv_x_leq sigma cl' cl then
-          let sg = mkGOAL info sign (DOP2(Cast,cl',cl'ty)) in
+    | { name = Convert_concl; terms = [cl'] } ->
+    	let cl'ty = type_of env sign cl' in
+	if is_conv_leq env cl' cl then
+          let sg = mk_goal info sign (DOP2(Cast,cl',cl'ty)) in
           [sg]
 	else 
 	  error "convert-concl rule passed non-converting term"
 
-    | {name=CONVERT_HYP;hypspecs=[id];terms=[ty']},
-      {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } ->
       (* Faut-il garder la sorte d'origine ou celle du converti ?? *)
-    	let tj = fexecute_type sigma (sign_before id sign) ty' in
-	if conv_x sigma ty' (snd(lookup_sign id sign)).body then
-          [mkGOAL info (modify_sign id tj sign) cl]
+    	let tj = execute_type env (sign_before id sign) ty' in
+	if is_conv env ty' (snd(lookup_sign id sign)).body then
+          [mk_goal info (modify_sign id tj sign) cl]
 	else 
 	  error "convert-hyp rule passed non-converting term"
 	    
-    | {name=THIN;hypspecs=ids}, {hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Thin; hypspecs = ids } ->
      	let rec remove_pair s = function
           | ([],[]) -> 
 	      error ((string_of_id s) ^ " is not among the assumptions.")
@@ -414,20 +377,23 @@ let prim_refiner r sigma goal =
             error ((string_of_id s) ^ " is used in the conclusion.");
           remove_pair s sign 
 	in
-     	let sg = mkGOAL info (List.fold_left clear_aux sign ids) cl in
+     	let sg = mk_goal info (List.fold_left clear_aux sign ids) cl in
      	[sg]
 
-    | {name=MOVE withdep;hypspecs=ids},{hyps=sign;concl=cl;info=(Some info)} ->
+    | { name = Move withdep; hypspecs = ids } ->
 	let (hfrom,hto) =
 	  match ids with [h1;h2] ->(h1,h2)| _ -> anomaly "prim_refiner:MOVE" in
   	let hyps = list_of_sign sign in
   	let (left,right,typfrom,toleft) = split_sign hfrom hto hyps in
   	let hyps' = 
 	  move_after withdep toleft (left,(hfrom,typfrom),right) hto in
-  	[mkGOAL info (make_sign hyps') cl]
+  	[mk_goal info (make_sign hyps') cl]
 	
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
-	  
+
+let abst_value c =
+  let env = Global.env () in
+  Environ.abst_value (Typing.unsafe_env_of_env env) c
 	  
 let extract_constr = 
   let rec crec vl = function
@@ -437,8 +403,8 @@ let extract_constr =
               | GLOBNAME (id,_) -> VAR id
               | RELNAME (n,_) -> Rel n)
          with Not_found -> 
-           (try search_reference vl str
-            with Not_found -> error((string_of_id str)^"  not declared")))
+           (try global_reference str
+            with Not_found -> error ((string_of_id str)^" not declared")))
 	
     | (Rel _) as val_0 -> val_0
 	  
@@ -446,21 +412,23 @@ let extract_constr =
         let u1 = crec vl c1 in
         DOP2(Lambda,u1,DLAM(na,crec (add_rel (Anonymous,u1) vl) c2))
 	  
-    | DOPN(Fix (x_0,x_1),cl) ->
+    | DOPN(Term.Fix (x_0,x_1),cl) ->
         let listar = Array.sub cl 0 ((Array.length cl) -1) 
-        and def = last_vect cl in 
+        and def = array_last cl in 
         let newar = Array.map (crec vl) listar in
         let newenv =
-          it_vect (fun env ar -> add_rel (Anonymous,ar) env) vl newar in
+          Array.fold_left
+	    (fun env ar -> add_rel (Anonymous,ar) env) vl newar in
         let newdef = under_dlams (crec newenv) def in 
-        DOPN(Fix (x_0,x_1),Array.append newar [|newdef|])
+        DOPN(Term.Fix (x_0,x_1),Array.append newar [|newdef|])
 	  
     | DOPN(CoFix par,cl) ->
         let listar = Array.sub cl 0 ((Array.length cl) -1) 
-        and def = last_vect cl in 
+        and def = array_last cl in 
         let newar = Array.map (crec vl) listar in
         let newenv =
-          it_vect (fun env ar -> add_rel (Anonymous,ar) env) vl newar in
+          Array.fold_left (fun env ar -> add_rel (Anonymous,ar) env) vl newar 
+	in
         let newdef = under_dlams (crec newenv) def in 
         DOPN(CoFix par,Array.append newar [|newdef|])
 	  
@@ -472,7 +440,6 @@ let extract_constr =
     | DOPN(Abst _,_) as val_0 -> crec vl (abst_value val_0)
     | DOPN(oper,cl) -> DOPN(oper,Array.map (crec vl) cl)
     | DOPL(oper,cl) -> DOPL(oper,List.map (crec vl) cl)
-    | DOP0(Implicit) -> anomaly "found a term Implicit in a construction"
     | DOP0(Meta _) as c -> c
     | DOP0 _ as c -> c
     | _ -> anomaly "extract_constr : term not matched"
@@ -480,88 +447,87 @@ let extract_constr =
   crec 
 
 
-let prim_extractor subfun vl = function
-    
-  | {ref=Some(PRIM{name=INTRO;newids=[id]},[spf]);
-     goal={concl=cl}} ->
-      (match strip_outer_cast cl with
-	 | DOP2(Prod,ty,b) ->
-	     let cty = extract_constr vl ty in
-             let na = Name id in 
-	     DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
-	 | _ -> error "incomplete proof!")
-
-  | {ref=Some(PRIM{name=INTRO_AFTER;newids=[id]},[spf]);
-     goal={concl=cl}} ->
-      (match strip_outer_cast cl with
-	 | DOP2(Prod,ty,b) ->
-	     let cty = extract_constr vl ty in
-             let na = Name id in 
-	     DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
-	 | _ -> error "incomplete proof!")
-      
-  | {ref=Some(PRIM{name=INTRO_REPLACING;hypspecs=[id]},[spf]);
-     goal={concl=cl}} ->
-      (match strip_outer_cast cl with
-	 | DOP2(Prod,ty,b) ->
-	     let cty = extract_constr vl ty in
-             let na = Name id in 
-	     DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
-	 | _ -> error "incomplete proof!")
-
-  | {ref=Some(PRIM{name=FIX;newids=[f];params=[Num(_,n)]},[spf]);
-     goal={concl=cl}} ->
-      let cty = extract_constr vl cl in 
-      let na = Name f in 
-      DOPN(Fix([|n-1|],0),
-	   [| cty ; DLAMV(na,[|subfun (add_rel (na,cty) vl) spf|])|])
-	
-  | {ref=Some(PRIM{name=FIX;newids=lf;terms=lar;params=ln},spfl);
-     goal={concl=cl}} ->
-      let lcty = List.map (extract_constr vl) (cl::lar) in 
-      let vn = Array.of_list (List.map (function Num(_,n) -> n-1
-					  | _ -> anomaly "mutual_fix_refiner")
-				ln) in 
-      let lna = List.map (fun f -> Name f) lf in
-      let newvl = List.fold_left2 (fun sign na ar -> (add_rel (na,ar) sign)) 
-                    vl lna lcty in 
-      let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
-      DOPN(Fix(vn,0),Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
-	
-  | {ref=Some(PRIM{name=COFIX;newids=lf;terms=lar},spfl);
-     goal={concl=cl}} ->
-      let lcty = List.map (extract_constr vl) (cl::lar) in 
-      let lna  = List.map (fun f -> Name f) lf in
-      let newvl = List.fold_left2 (fun sign na ar -> (add_rel (na,ar) sign)) 
-                    vl lna lcty in 
-      let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
-      DOPN(CoFix(0),Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
+let prim_extractor subfun vl pft =
+  let cl = pft.goal.goal_ev.evar_concl in
+  match pft with
+    | { ref = Some (Prim { name = Intro; newids = [id] }, [spf]) } ->
+	(match strip_outer_cast cl with
+	   | DOP2(Prod,ty,b) ->
+	       let cty = extract_constr vl ty in
+               let na = Name id in 
+	       DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
+	   | _ -> error "incomplete proof!")
 	
-  | {ref=Some(PRIM{name=REFINE;terms=[c]},spfl);
-     goal={concl=cl}} ->
-      let mvl = collect_meta_variables c in
-      let metamap = List.combine mvl (List.map (subfun vl) spfl) in
-      let cc = extract_constr vl c in 
-      plain_instance metamap cc
+    | { ref = Some (Prim { name = Intro_after; newids = [id]}, [spf]) } -> 
+	(match strip_outer_cast cl with
+	   | DOP2(Prod,ty,b) ->
+	       let cty = extract_constr vl ty in
+               let na = Name id in 
+	       DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
+	   | _ -> error "incomplete proof!")
 	
-  | {ref=Some(PRIM{name=CONVERT_CONCL;terms=[c]},[pf])} ->
-      subfun vl pf
+    | {ref=Some(Prim{name=Intro_replacing;hypspecs=[id]},[spf]) } ->
+	(match strip_outer_cast cl with
+	   | DOP2(Prod,ty,b) ->
+	       let cty = extract_constr vl ty in
+               let na = Name id in 
+	       DOP2(Lambda,cty,DLAM(na,subfun (add_rel (na,cty) vl) spf))
+	   | _ -> error "incomplete proof!")
 	
-  | {ref=Some(PRIM{name=CONVERT_HYP;hypspecs=[id];terms=[c]},[pf])} ->
-      subfun vl pf
+    | {ref=Some(Prim{name=Fix;newids=[f];params=[Num(_,n)]},[spf]) } -> 
+	let cty = extract_constr vl cl in 
+	let na = Name f in 
+	DOPN(Term.Fix([|n-1|],0),
+	     [| cty ; DLAMV(na,[|subfun (add_rel (na,cty) vl) spf|])|])
+	  
+    | {ref=Some(Prim{name=Fix;newids=lf;terms=lar;params=ln},spfl) } ->
+	let lcty = List.map (extract_constr vl) (cl::lar) in 
+	let vn = 
+	  Array.of_list (List.map (function Num(_,n) -> n-1
+				     | _ -> anomaly "mutual_fix_refiner")
+			   ln) 
+	in 
+	let lna = List.map (fun f -> Name f) lf in
+	let newvl = List.fold_left2 (fun sign na ar -> (add_rel (na,ar) sign)) 
+                      vl lna lcty in 
+	let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
+	DOPN(Term.Fix(vn,0),
+	     Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
 	
-  | {ref=Some(PRIM{name=THIN;hypspecs=ids},[pf])} ->
-      subfun vl pf
+    | {ref=Some(Prim{name=Cofix;newids=lf;terms=lar},spfl) } ->
+	let lcty = List.map (extract_constr vl) (cl::lar) in 
+	let lna  = List.map (fun f -> Name f) lf in
+	let newvl = 
+	  List.fold_left2 (fun sign na ar -> (add_rel (na,ar) sign)) 
+            vl lna lcty 
+	in 
+	let lfix =Array.map (subfun newvl) (Array.of_list spfl) in
+	DOPN(CoFix(0),Array.of_list (lcty@[put_DLAMSV (List.rev lna) lfix]))
+	  
+    | {ref=Some(Prim{name=Refine;terms=[c]},spfl) } ->
+	let mvl = collect_meta_variables c in
+	let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+	let cc = extract_constr vl c in 
+	plain_instance metamap cc
+	  
+    | {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} ->
+	subfun vl pf
 	
-  | {ref=Some(PRIM{name=MOVE _;hypspecs=ids},[pf])} ->
-      subfun vl pf
+    | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[c]},[pf])} ->
+	subfun vl pf
 	
-  | {ref=Some(PRIM _,_)} ->
-      error "prim_extractor handed unrecognizable primitive proof"
+    | {ref=Some(Prim{name=Thin;hypspecs=ids},[pf])} ->
+	subfun vl pf
 	
-  | {ref=None} -> error "prim_extractor handed incomplete proof"
-
-  | _ -> anomaly "prim_extractor"
+    | {ref=Some(Prim{name=Move _;hypspecs=ids},[pf])} ->
+	subfun vl pf
+	  
+    | {ref=Some(Prim _,_)} ->
+	error "prim_extractor handed unrecognizable primitive proof"
+	  
+    | {ref=None} -> error "prim_extractor handed incomplete proof"
+	  
+    | _ -> anomaly "prim_extractor"
 	
 (***
 let prim_extractor = Profile.profile3 "prim_extractor" prim_extractor
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 5ce323ed95..27a50af85b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -2,15 +2,13 @@
 (* $Id$ *)
 
 (*i*)
-open Pp
 open Term
 open Sign
+open Environ
 open Proof_trees
 (*i*)
 
-val pr_prim_rule : prim_rule -> std_ppcmds
-
-val prim_refiner : prim_rule -> Evd.evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> unsafe_env -> goal -> goal list
 
 val prim_extractor : 
   ((typed_type, constr) env -> proof_tree -> constr) -> 
diff --git a/proofs/tmp-src b/proofs/tmp-src
index eca0119b18..1da11fe01d 100644
--- a/proofs/tmp-src
+++ b/proofs/tmp-src
@@ -25,103 +25,11 @@ let existential_value env k =
 
 (******* 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. *)
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6ed2851e34..ea440788b6 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -213,4 +213,23 @@ let explain_type_error k ctx = function
   | IllTypedRecBody (i, lna, vdefj, vargs) ->
       explain_ill_typed_rec_body k ctx i lna vdefj vargs
 
+let explain_refiner_bad_type k ctx arg ty conclty =
+  errorlabstrm "Logic.conv_leq_goal"
+    [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
+       P.pr_term k ctx arg; 'sPC;
+       'sTR"of type"; 'bRK(1,1); P.pr_term k ctx ty; 'sPC;
+       'sTR"instead of"; 'bRK(1,1); P.pr_term k ctx conclty >]
+
+let explain_refiner_occur_meta k ctx t =
+  errorlabstrm "Logic.mk_refgoals"
+    [< 'sTR"cannot refine with term"; 'bRK(1,1); P.pr_term k ctx t;
+       'sPC; 'sTR"because there are metavariables, and it is";
+       'sPC; 'sTR"neither an application nor a Case" >]
+
+let explain_refiner_cannot_applt k ctx t harg =
+  errorlabstrm "Logic.mkARGGOALS"
+    [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
+       P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+       P.pr_term k ctx harg >]
+
 end