Backtrack sur modif Evd.evd_concl

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

9 files changed, 18 insertions, 13 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
index b12e6e9930..b31f2f6b79 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -20,7 +20,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : typed_type;
+  evar_concl : constr;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 036443f129..62378f921e 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -23,7 +23,7 @@ type evar_body =
   | Evar_defined of constr
 
 type 'a evar_info = {
-  evar_concl : typed_type;
+  evar_concl : constr;
   evar_env : unsafe_env;
   evar_body : evar_body;
   evar_info : 'a }
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 37ffa5ca12..f3634eac5b 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -82,7 +82,7 @@ let existential_type sigma c =
   let (n,args) = destEvar c in
   let info = Evd.map sigma n in
   let hyps = evar_hyps info in
-  instantiate_constr (ids_of_sign hyps) (body_of_type info.evar_concl)
+  instantiate_constr (ids_of_sign hyps) info.evar_concl
     (Array.to_list args)
 
 let existential_value sigma c =
diff --git a/kernel/term.ml b/kernel/term.ml
index 72d6cfbd2e..f7b7b607fd 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -72,6 +72,10 @@ let body_of_type ty = ty.body
 
 let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
 
+let outcast_type = function
+   DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s}
+  | _ -> anomaly "outcast_type: Not an in-casted type judgement"
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index 5118d39c5d..194681154a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -62,6 +62,8 @@ val body_of_type : typed_type -> constr
 
 val incast_type : typed_type -> constr
 
+val outcast_type : constr -> typed_type
+
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f20c5d213a..d224b0209e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -181,7 +181,7 @@ let type_of_existential env sigma c =
   let hyps = get_globals (context evi.Evd.evar_env) in
   let id = id_of_string ("?" ^ string_of_int ev) in
   check_hyps id env sigma hyps;
-  instantiate_type (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
+  instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
 
 
 (* Case. *)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 1e602e0397..ddf09ab348 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -32,7 +32,7 @@ val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type
 
 val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr
 
-val type_of_existential : unsafe_env -> 'a evar_map -> constr -> typed_type
+val type_of_existential : unsafe_env -> 'a evar_map -> constr -> constr
 
 val type_of_case : unsafe_env -> 'a evar_map 
   -> unsafe_judgment -> unsafe_judgment 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 11f978d4dc..b0823c1b2d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -221,7 +221,7 @@ let prim_refiner r sigma goal =
   match r with
     | { name = Intro; newids = [id] } ->
     	if mem_sign sign id then error "New variable is already declared";
-        (match strip_outer_cast cl.body with
+        (match strip_outer_cast cl with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       let a = mk_assumption env sigma c1
@@ -232,7 +232,7 @@ let prim_refiner r sigma goal =
 	
     | { name = Intro_after; newids = [id]; hypspecs = [whereid] } ->
     	if mem_sign sign id then error "New variable is already declared";
-        (match strip_outer_cast cl.body with
+        (match strip_outer_cast cl with
 	   | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       if not (List.for_all
@@ -248,7 +248,7 @@ let prim_refiner r sigma goal =
 	   | _ -> error "Introduction needs a product")
 	
     | { name = Intro_replacing; newids = []; hypspecs = [id] } ->
-	(match strip_outer_cast cl.body with
+	(match strip_outer_cast cl with
            | DOP2(Prod,c1,b) ->
 	       if occur_meta c1 then error_use_instantiate();
 	       if not (List.for_all 
@@ -280,10 +280,10 @@ let prim_refiner r sigma goal =
 		  check_ind (k-1) b
             | _ -> error "not enough products"
 	in
-     	let _ = check_ind n cl.body in 
+     	let _ = check_ind n cl in 
 	if mem_sign sign f then error "name already used in the environment";
-        let a = mk_assumption env sigma cl.body in
-        let sg = mk_goal info (push_var (f,a) env) cl.body in
+        let a = mk_assumption env sigma cl in
+        let sg = mk_goal info (push_var (f,a) env) cl in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index a119354a01..3523f42182 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -96,8 +96,7 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt env cl = 
-  let ty = execute_type env Evd.empty cl in
-  { evar_env = env; evar_concl = ty; evar_body = Evar_empty; evar_info = ctxt }
+  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)