- Typing -> Safe_typing

 - proofs/Typing_ev -> pretyping/Typing
 - env -> sign
 - fonctions var_context


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

10 files changed, 27 insertions, 188 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4c14040bdd..80aae11823 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -33,7 +33,7 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let hyps = get_globals (Environ.context env) in
+  let hyps = Environ.var_context env in
   let ev = new_evar () in
   DOPN(Evar ev,
        Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)))
@@ -881,10 +881,10 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
-  failwith "TODO: clenv_type_of"
+  failwith "TODO"
   (***
-  (Trad.ise_resolve true (w_Underlying ce.hook) metamap
-     (gLOB(w_hyps ce.hook)) c)._TYPE
+  (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
+     (gLOB(w_hyps ce.hook)) c).uj_type
   ***)
 
 let clenv_instance_type_of ce c =
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f3421cfdcc..e63648576d 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -10,7 +10,7 @@ open Term
 open Environ
 open Evd
 open Reduction
-open Typing_ev
+open Typing
 open Proof_trees
 open Logic
 open Refiner
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b0823c1b2d..f89c6e9b4e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -10,7 +10,7 @@ open Term
 open Sign
 open Environ
 open Reduction
-open Typing_ev
+open Typing
 open Proof_trees
 open Typeops
 open Coqast
@@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto =
 
 let prim_refiner r sigma goal =
   let env = goal.evar_env in
-  let sign = get_globals (context env) in
+  let sign = var_context env in
   let cl = goal.evar_concl in
   let info = goal.evar_info in
   match r with
@@ -401,8 +401,8 @@ let prim_refiner r sigma goal =
     | _ -> anomaly "prim_refiner: Unrecognized primitive rule"
 
 let abst_value c =
-  let env = Global.env () in
-  Environ.abst_value (Typing.unsafe_env_of_env env) c
+  let env = Global.unsafe_env () in
+  Environ.abst_value env c
 	  
 let extract_constr = 
   let rec crec vl = function
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2b2f9b8b44..88b632882e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -15,8 +15,8 @@ open Proof_trees
 val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list
 
 val prim_extractor : 
-  ((typed_type, constr) env -> proof_tree -> constr) -> 
-    (typed_type, constr) env -> proof_tree -> constr
+  ((typed_type, constr) sign -> proof_tree -> constr) -> 
+    (typed_type, constr) sign -> proof_tree -> constr
 
 val extract_constr : constr assumptions -> constr -> constr
 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 3523f42182..ee0f3de895 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,7 +8,7 @@ open Sign
 open Evd
 open Stamps
 open Environ
-open Typing_ev
+open Typing
 
 type bindOcc = 
   | Dep of identifier
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 834ee67343..1dc43f4134 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -714,7 +714,7 @@ let extract_pftreestate pts =
       [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ;
          'sPC; 'sTR"Please ascend to the root" >];
   let env = pts.tpf.goal.evar_env in
-  let hyps = get_globals (Environ.context env) in
+  let hyps = Environ.var_context env in
   strong whd_betadeltatiota env (ts_it pts.tpfsigma)
     (extract_proof hyps pts.tpf)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8bb6fba486..85f2973c03 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -11,7 +11,7 @@ open Instantiate
 open Environ
 open Reduction
 open Evd
-open Typing_ev
+open Typing
 open Tacred
 open Proof_trees
 open Logic
@@ -45,7 +45,7 @@ let pf_concl gls = (sig_it gls).evar_concl
 
 let pf_untyped_hyps gls  =
   let env = pf_env gls in
-  let (idl,tyl) = get_globals (Environ.context env) in 
+  let (idl,tyl) = Environ.var_context env in 
   (idl, List.map (fun x -> x.body) tyl)
 
 let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n
@@ -69,6 +69,14 @@ let hnf_type_of gls =
 let pf_check_type gls c1 c2 =
   let casted = mkCast c1 c2 in pf_type_of gls casted
 
+let pf_constr_of_com gls c =
+  let evc = project gls in 
+  Astterm.constr_of_com evc (sig_it gls).hyps c
+
+let pf_constr_of_com_sort gls c =
+  let evc = project gls in 
+  Astterm.constr_of_com_sort evc (sig_it gls).hyps c
+
 let pf_reduction_of_redexp gls re c = 
   reduction_of_redexp re (pf_env gls) (project gls) c 
 
@@ -242,7 +250,7 @@ let mutual_cofix lf lar pf =
     
 let rename_bound_var_goal gls =
   let { evar_env = env; evar_concl = cl } as gl = sig_it gls in 
-  let ids = ids_of_sign (get_globals (Environ.context env)) in
+  let ids = ids_of_sign (Environ.var_context env) in
   convert_concl (rename_bound_var ids cl) gls
     
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 863023b79a..ea13c75a79 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,6 +41,9 @@ val pf_check_type         : goal sigma -> constr -> constr -> constr
 val pf_fexecute           : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> constr
 
+val pf_constr_of_com      : goal sigma -> Coqast.t -> constr
+val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr
+
 val pf_get_hyp             : goal sigma -> identifier -> constr
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
deleted file mode 100644
index 741ef10409..0000000000
--- a/proofs/typing_ev.ml
+++ /dev/null
@@ -1,154 +0,0 @@
-
-(* $Id$ *)
-
-open Util
-open Names
-open Generic
-open Term
-open Environ
-open Reduction
-open Type_errors
-open Typeops
-
-let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
-
-type 'a mach_flags = {
-  fix : bool;
-  nocheck : bool }
-
-(* The typing machine without information, without universes but with
-   existential variables. *)
-
-let rec execute mf env sigma cstr =
-  match kind_of_term cstr with
-    | IsMeta n ->
-	error "execute: found a non-instanciated goal"
-
-    | IsEvar _ ->
-	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
-
-    | IsVar id -> 
-	make_judge cstr (snd (lookup_var id env))
-	  
-    | IsAbst _ ->
-        if evaluable_abst env cstr then 
-	  execute mf env sigma (abst_value env cstr)
-        else 
-	  error "Cannot typecheck an unevaluable abstraction"
-	      
-    | IsConst _ ->
-        make_judge cstr (type_of_constant env sigma cstr)
-	  
-    | IsMutInd _ ->
-	make_judge cstr (type_of_inductive env sigma cstr)
-	  
-    | IsMutConstruct _ -> 
-	let (typ,kind) = destCast (type_of_constructor env sigma cstr) in
-        { uj_val = cstr; uj_type = typ; uj_kind = kind }
-	  
-    | IsMutCase (_,p,c,lf) ->
-        let cj = execute mf env sigma c in
-        let pj = execute mf env sigma p in
-        let lfj = execute_array mf env sigma lf in
-        type_of_case env sigma pj cj lfj
-  
-    | IsFix (vn,i,lar,lfi,vdef) ->
-        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
-          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 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 cofix;
-	make_judge cofix larv.(i)
-	  
-    | IsSort (Prop c) -> 
-	make_judge_of_prop_contents c
-
-    | IsSort (Type u) ->
-	let (j,_) = make_judge_of_type u in j
-	  
-    | IsAppL (f,args) ->
-	let j = execute mf env sigma f in
-        let jl = execute_list mf env sigma args in
-	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
-	j
-	    
-    | IsLambda (name,c1,c2) -> 
-        let j = execute mf env sigma c1 in
-        let var = assumption_of_judgment env sigma j in
-	let env1 = push_rel (name,var) env in
-        let j' = execute mf env1 sigma c2 in 
-        let (j,_) = abs_rel env1 sigma name var j' in
-	j
-	  
-    | IsProd (name,c1,c2) ->
-        let j = execute mf env sigma c1 in
-        let var = assumption_of_judgment env sigma j in
-	let env1 = push_rel (name,var) env in
-        let j' = execute mf env1 sigma c2 in
-	let (j,_) = gen_rel env1 sigma name var j' in
-	j
-	  
-    | IsCast (c,t) ->
-        let cj = execute mf env sigma c in
-        let tj = execute mf env sigma t in
-        cast_rel env sigma cj tj
-	  
-      | _ -> error_cant_execute CCI env cstr
-	  
-and execute_fix mf env sigma lar lfi vdef =
-  let larj = execute_array mf env sigma lar in
-  let lara = Array.map (assumption_of_judgment env sigma) larj in
-  let nlara = 
-    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
-  let env1 = 
-    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
-  let vdefj = execute_array mf env1 sigma vdef in
-  let vdefv = Array.map j_val_only vdefj in
-  let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
-  (lara,vdefv)
-
-and execute_array mf env sigma v =
-  let jl = execute_list mf env sigma (Array.to_list v) in
-  Array.of_list jl
-
-and execute_list mf env sigma = function
-  | [] -> 
-      []
-  | c::r -> 
-      let j = execute mf env sigma c in 
-      let jr = execute_list mf env sigma r in
-      j::jr
-
-
-let safe_machine env sigma constr = 
-  let mf = { fix = false; nocheck = false } in
-  execute mf env sigma constr
-
-
-(* Type of a constr *)
-
-let type_of env sigma c = 
-  let j = safe_machine env sigma c in 
-  nf_betaiota env sigma j.uj_type
-
-(* The typed type of a judgment. *)
-
-let execute_type env sigma constr = 
-  let j = execute { fix=false; nocheck=true } env sigma constr in
-  assumption_of_judgment env sigma j
-
-let execute_type env sigma constr = 
-  let j = execute { fix=false; nocheck=false } env sigma constr in
-  assumption_of_judgment env sigma j
diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli
deleted file mode 100644
index b12cd369d3..0000000000
--- a/proofs/typing_ev.mli
+++ /dev/null
@@ -1,18 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Term
-open Environ
-open Evd
-(*i*)
-
-(* This module provides the typing machine with existential variables
-   (but without universes). *)
-
-val type_of : unsafe_env -> 'a evar_map -> constr -> constr
-
-val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type
-
-val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type
-