MAJ pour fusion avec pretyping

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

3 files changed, 13 insertions, 11 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b0823c1b2d..11f978d4dc 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 with
+        (match strip_outer_cast cl.body 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 with
+        (match strip_outer_cast cl.body 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 with
+	(match strip_outer_cast cl.body 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 in 
+     	let _ = check_ind n cl.body in 
 	if mem_sign sign f then error "name already used in the environment";
-        let a = mk_assumption env sigma cl in
-        let sg = mk_goal info (push_var (f,a) env) cl in
+        let a = mk_assumption env sigma cl.body in
+        let sg = mk_goal info (push_var (f,a) env) cl.body in
         [sg]
     
     | { name = Fix; hypspecs = []; terms = lar; newids = lf; params = ln } ->
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index d12dad6e25..a119354a01 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,6 +8,7 @@ open Sign
 open Evd
 open Stamps
 open Environ
+open Typing_ev
 
 type bindOcc = 
   | Dep of identifier
@@ -95,7 +96,8 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt env cl = 
-  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
+  let ty = execute_type env Evd.empty cl in
+  { evar_env = env; evar_concl = ty; evar_body = Evar_empty; evar_info = ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
index 6bf2dd9119..54a9d42dce 100644
--- a/proofs/typing_ev.ml
+++ b/proofs/typing_ev.ml
@@ -60,20 +60,20 @@ let rec execute mf env sigma cstr =
           error "General Fixpoints not allowed";
         let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
         let fix = mkFix vn i larv lfi vdefv in
-        check_fix env sigma Spset.empty fix;
+        check_fix env sigma fix;
 	make_judge fix larv.(i)
 	  
     | IsCoFix (i,lar,lfi,vdef) ->
         let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
         let cofix = mkCoFix i larv lfi vdefv in
-        check_cofix env sigma Spset.empty cofix;
+        check_cofix env sigma cofix;
 	make_judge cofix larv.(i)
 	  
     | IsSort (Prop c) -> 
-	type_of_prop_or_set c
+	make_judge_of_prop_contents c
 
     | IsSort (Type u) ->
-	let (j,_) = type_of_type u in j
+	let (j,_) = make_judge_of_type u in j
 	  
     | IsAppL (f,args) ->
 	let j = execute mf env sigma f in