Canonisation de certains noms dans Pretyping, Asterm et Safe_typing

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

4 files changed, 22 insertions, 14 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 60d9e5f13..7da510029 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -8,6 +8,7 @@ open Generic
 open Term
 open Declarations
 open Inductive
+open Environ
 open Reduction
 open Tacred
 open Declare
@@ -144,8 +145,9 @@ let build_mutual lparams lnamearconstrs finite =
     let (ind_env,arityl) =
       List.fold_left 
 	(fun (env,arl) (recname,arityc,_) -> 
-           let arity =
-	     typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
+           let raw_arity = mkProdCit lparams arityc in
+           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
+	   let arity = Typeops.assumption_of_type_judgment arj in
 	   let env' = Environ.push_rel_decl (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
@@ -218,8 +220,11 @@ let build_recursive lnameargsardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,lparams,arityc,_) -> 
-           let arity = typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
-           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           let raw_arity = mkProdCit lparams arityc in
+           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
+	   let arity = Typeops.assumption_of_type_judgment arj in
+           declare_variable recname
+	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
@@ -281,8 +286,10 @@ let build_corecursive lnameardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
-           let arity = typed_type_of_com Evd.empty env0 arityc in
-           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
+	   let arity = Typeops.assumption_of_type_judgment arj in
+           declare_variable recname
+	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 5df900c26..945ff63ef 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -44,7 +44,7 @@ let rec globalize bv = function
 
 let check c = 
   let c = globalize [] c in
-  let (j,u) = safe_machine !env c in
+  let (j,u) = safe_infer !env c in
   let ty = j_type j in
   let pty = pr_term CCI (env_of_safe_env !env) ty in
   mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 pty; 'fNL >])
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0fc6f85a8..9801045a2 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -71,15 +71,17 @@ let typecheck_params_and_field ps fs =
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newps))
+         let tj = type_judgment_of_rawconstr Evd.empty env t in
+	 let ass = Typeops.assumption_of_type_judgment tj in
+         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
-         let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newfs)) (env1,[]) fs
+         let tj = type_judgment_of_rawconstr Evd.empty env t in
+	 let ass = Typeops.assumption_of_type_judgment tj in
+         (Environ.push_var_decl (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 32a30d144..4010c8359 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -813,7 +813,7 @@ let _ =
        | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
            let (evmap,sign) = get_current_context_of_args g in
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
-	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
+	   fun () -> mSG (redfun (judgment_of_rawconstr evmap sign c))
        | _ -> bad_vernac_args "Eval")
 
 let _ =
@@ -825,8 +825,7 @@ let _ =
 	     | "CHECK" -> print_val
              | "PRINTTYPE" -> print_type
              | _ -> anomaly "Unexpected string" 
-	   in
-	   (fun () -> mSG (prfun sign (judgment_of_com evmap sign c)))
+	   in (fun () -> mSG (prfun sign (judgment_of_rawconstr evmap sign c)))
        | _ -> bad_vernac_args "Check")
 
 (***