typage des existentielles dans Typing_ev; suppression metamap inutiles dans typage

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

7 files changed, 11 insertions, 11 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f715e985aa..34261e7355 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ let empty_env = {
 
 let universes env = env.env_universes
 let context env = env.env_context
-let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 
 (* Construction functions. *)
 
diff --git a/kernel/evd.ml b/kernel/evd.ml
index b31f2f6b79..52e1a936eb 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -65,6 +65,4 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let metamap sigma = failwith "metamap : NOT YET IMPLEMENTED"
-
 let evar_hyps ev = get_globals (context ev.evar_env)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 62378f921e..2e55f578e9 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -48,6 +48,4 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val metamap : 'a evar_map -> (int * constr) list
-
 val evar_hyps : 'a evar_info -> typed_type signature
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 89aa184274..834ee67343 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -159,7 +159,7 @@ let refiner = function
               subproof = Some hidden_proof;
               ref = Some(r,spfl) }))
       
-  | ((Context ctxt) as r) ->
+  | (Context ctxt) as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it in
          let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
@@ -174,7 +174,7 @@ let refiner = function
       
    (* [Local_constraints lc] makes the local constraints be [lc] *)
 
-  | ((Local_constraints lc) as r) ->
+  | (Local_constraints lc) as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
          let ctxt = gl.evar_info in 
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
index 54a9d42dce..5e48153719 100644
--- a/proofs/typing_ev.ml
+++ b/proofs/typing_ev.ml
@@ -22,10 +22,13 @@ type 'a mach_flags = {
 
 let rec execute mf env sigma cstr =
   match kind_of_term cstr with
-    | IsMeta _ ->
-	anomaly "the kernel does not understand metas"
+    | IsMeta n ->
+	error "execute: found a non-instanciated goal"
+
     | IsEvar _ ->
-	anomaly "the kernel does not understand existential variables"
+	let ty = type_of_existential env sigma cstr in
+	let jty = execute mf env sigma ty in
+	{ uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
 	
     | IsRel n -> 
 	relative env n
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 44f17e8165..e541c29dbd 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -19,6 +19,8 @@ open Clenv
    write to Eduardo.Gimenez@inria.fr and ask for the prize :-)
    -- Eduardo (11/8/97) *)
 
+type wc = walking_constraints
+
 let pf_get_new_id id gls = 
   next_ident_away id (ids_of_sign (pf_untyped_hyps gls))
 
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 8aee8dcb7c..b1bf17e015 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -46,7 +46,7 @@ val res_pf_THEN_i :
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
     int -> tactic
 
-val elim_res_pf_THEN_id : 
+val elim_res_pf_THEN_i : 
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> 
     int -> tactic