Simplifications autour de typed_type (renommé types par analogie avec sorts); documentation

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

4 files changed, 18 insertions, 22 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6150f0c024..6d8264d9c8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -140,7 +140,7 @@ let build_mutual lparams lnamearconstrs finite =
 	(fun (env,arl) (recname,arityc,_) -> 
            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 arity = arj.utj_val in
 	   let env' = Environ.push_rel_assum (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
@@ -215,7 +215,7 @@ let build_recursive lnameargsardef =
         (fun (env,arl) (recname,lparams,arityc,_) -> 
            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 arity = arj.utj_val in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
@@ -239,7 +239,7 @@ let build_recursive lnameargsardef =
   if lnamerec <> [] then begin
     let recvec = 
       Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
-    let varrec = Array.of_list (List.map incast_type larrec) in
+    let varrec = Array.of_list larrec in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
@@ -283,7 +283,7 @@ let build_corecursive lnameardef =
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
            let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
-	   let arity = Typeops.assumption_of_type_judgment arj in
+	   let arity = arj.utj_val in
            declare_variable recname
 	     (SectionLocalDecl arj.utj_val,NeverDischarge,false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
@@ -310,7 +310,7 @@ let build_corecursive lnameardef =
 	[||] 
       else 
 	Array.map (subst_vars (List.rev lnamerec)) (Array.of_list ldefrec) in
-    let varrec = Array.of_list (List.map incast_type larrec) in
+    let varrec = Array.of_list larrec in
     let rec declare i = function 
       | fi::lf ->
 	  let ce = 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2cfd2ca647..f25861d88a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -26,8 +26,6 @@ let recalc_sp sp =
 
 let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
 
-let generalize_type = generalize_without_universes
-
 type modification_action = ABSTRACT | ERASE
 
 let interp_modif absfun oper (oper',modif) cl = 
@@ -129,11 +127,9 @@ let abstract_inductive ids_to_abs hyps inds =
     let inds' =
       List.map
       	(function (tname,arity,cnames,lc) -> 
-	   let arity' = generalize_type d arity in
+	   let arity' = mkNamedProd_or_LetIn d arity in
 	   let lc' =
-	     List.map
-	       (fun b -> generalize_type d (typed_app (substl new_refs) b))
-	       lc
+	     List.map (fun b -> mkNamedProd_or_LetIn d (substl new_refs b)) lc
 	   in
            (tname,arity',cnames,lc'))
       	inds
@@ -171,7 +167,7 @@ let abstract_constant ids_to_abs hyps (body,typ) =
 	| Some { contents = Recipe f } ->
 	    Some (ref (Recipe (fun () -> mkNamedLambda_or_LetIn decl (f()))))
       in
-      let typ' = generalize_type decl typ in
+      let typ' = mkNamedProd_or_LetIn decl typ in
       (rest, body', typ', ABSTRACT::modl)
   in
   let (_,body',typ',revmodl) =
@@ -206,8 +202,8 @@ let expmod_constr oldenv modlist c =
     | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'
 
-let expmod_type oldenv modlist c = 
-  typed_app (expmod_constr oldenv modlist) c
+let expmod_type oldenv modlist c =
+  type_app (expmod_constr oldenv modlist) c
 
 let expmod_constant_value opaque oldenv modlist = function
   | None -> None
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 0ba0e73a70..5680af6f57 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -51,7 +51,7 @@ val explain_ill_formed_branch :
   path_kind -> env -> constr -> int -> constr -> constr -> std_ppcmds
 
 val explain_generalization :
-  path_kind -> env -> name * typed_type -> constr -> std_ppcmds
+  path_kind -> env -> name * types -> constr -> std_ppcmds
 
 val explain_actual_type :
   path_kind -> env -> constr -> constr -> constr -> std_ppcmds
@@ -62,6 +62,6 @@ val explain_ill_formed_rec_body :
 
 val explain_ill_typed_rec_body  :
   path_kind -> env -> int -> name list -> unsafe_judgment array 
-    -> typed_type array -> std_ppcmds
+    -> types array -> std_ppcmds
 
 end
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 321f9bf31b..38d9e670db 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -66,22 +66,22 @@ let all_vars t =
 let print_id_list l = 
   [< 'sTR "[" ; prlist_with_sep pr_coma print_id l; 'sTR "]" >]
 
+open Environ
+
 let typecheck_params_and_field ps fs =
   let env0 = Global.env () in
   let env1,newps =
     List.fold_left
       (fun (env,newps) (id,t) -> 
-         let tj = type_judgment_of_rawconstr Evd.empty env t in
-	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newps))
+         let tj = interp_type Evd.empty env t in
+         (push_named_assum (id,tj) env,(id,tj)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
-         let tj = type_judgment_of_rawconstr Evd.empty env t in
-	 let ass = Typeops.assumption_of_type_judgment tj in
-         (Environ.push_named_assum (id,ass) env,(id,tj.Environ.utj_val)::newfs)) (env1,[]) fs
+         let ass = interp_type Evd.empty env t in
+         (push_named_assum (id,ass) env,(id,ass)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)