Moved code from Pretype_error to Evarutil

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

5 files changed, 32 insertions, 44 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fcc284832..0c339df4e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -36,11 +36,28 @@ let rec flush_and_check_evars sigma c =
        | Some c -> flush_and_check_evars sigma c)
   | _ -> map_constr (flush_and_check_evars sigma) c
 
-let nf_evar = Pretype_errors.nf_evar
-let j_nf_evar = Pretype_errors.j_nf_evar
-let jl_nf_evar = Pretype_errors.jl_nf_evar
-let jv_nf_evar = Pretype_errors.jv_nf_evar
-let tj_nf_evar = Pretype_errors.tj_nf_evar
+let nf_evar = Reductionops.nf_evar
+let j_nf_evar sigma j =
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = nf_evar sigma j.uj_type }
+let j_nf_betaiotaevar sigma j =
+  { uj_val = nf_evar sigma j.uj_val;
+    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
+let tj_nf_evar sigma {utj_val=v;utj_type=t} =
+  {utj_val=nf_evar sigma v;utj_type=t}
+
+let env_nf_evar sigma env =
+  process_rel_context
+    (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
+
+let env_nf_betaiotaevar sigma env =
+  process_rel_context
+    (fun d e ->
+      push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
 
 let nf_named_context_evar sigma ctx =
   Sign.map_named_context (Reductionops.nf_evar sigma) ctx
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9c6f1ad47..5c32a9a5c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -184,6 +184,14 @@ val nf_evar_info : evar_map -> evar_info -> evar_info
 val nf_evar_map : evar_map -> evar_map
 val nf_evar_map_undefined : evar_map -> evar_map
 
+val env_nf_evar : evar_map -> env -> env
+val env_nf_betaiotaevar : evar_map -> env -> env
+
+val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment
+val jv_nf_betaiotaevar :
+  evar_map -> unsafe_judgment array -> unsafe_judgment array
+(** Presenting terms without solved evars *)
+
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
 val flush_and_check_evars :  evar_map -> constr -> constr
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ad6922dbe..19ccb2375 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -45,29 +45,6 @@ let precatchable_exception = function
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
-let nf_evar = Reductionops.nf_evar
-let j_nf_evar sigma j =
-  { uj_val = nf_evar sigma j.uj_val;
-    uj_type = nf_evar sigma j.uj_type }
-let j_nf_betaiotaevar sigma j =
-  { uj_val = nf_evar sigma j.uj_val;
-    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
-let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jv_nf_betaiotaevar sigma jl =
-  Array.map (j_nf_betaiotaevar sigma) jl
-let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
-let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=nf_evar sigma v;utj_type=t}
-
-let env_nf_evar sigma env =
-  process_rel_context
-    (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
-
-let env_nf_betaiotaevar sigma env =
-  process_rel_context
-    (fun d e ->
-      push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
-
 (* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 558f3d5bb..3a4c6aad5 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -43,20 +43,6 @@ exception PretypeError of env * Evd.evar_map * pretype_error
 
 val precatchable_exception : exn -> bool
 
-(** Presenting terms without solved evars *)
-val nf_evar : Evd.evar_map -> constr -> constr
-val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jl_nf_evar : Evd.evar_map -> unsafe_judgment list -> unsafe_judgment list
-val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-
-val env_nf_evar : Evd.evar_map -> env -> env
-val env_nf_betaiotaevar : Evd.evar_map -> env -> env
-
-val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
-val jv_nf_betaiotaevar :
-  Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
-
 (** Raising errors *)
 val error_actual_type_loc :
   Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 0f9100e79..5ae04488f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -205,12 +205,12 @@ let rec execute env evdref cstr =
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
-		    (jv_nf_evar !evdref jl))
+		    (Evarutil.jv_nf_evar !evdref jl))
 	    | Const cst ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
-		    (jv_nf_evar !evdref jl))
+		    (Evarutil.jv_nf_evar !evdref jl))
 	    | _ ->
 		execute env evdref f
 	in