Move generally useful definition of nf_evar on contexts to evarutil.

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

4 files changed, 15 insertions, 15 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 112c2fc189..8a0b940b1a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -264,14 +264,3 @@ let implicits_of_rawterm l =
       | RLetIn (loc, na, t, b) -> aux i b
       | _ -> []
   in aux 1 l
-
-let nf_named_context sigma ctx = 
-  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
-
-let nf_rel_context sigma ctx = 
-  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
-    
-let nf_env sigma env = 
-  let nc' = nf_named_context sigma (Environ.named_context env) in
-  let rel' = nf_rel_context sigma (Environ.rel_context env) in
-    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index ab23e763c1..4ea95fc43c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -54,10 +54,6 @@ val implicits_of_binders : local_binder list -> (Topconstr.explicitation * (bool
 
 val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
 
-val nf_named_context : evar_map -> named_context -> named_context
-val nf_rel_context : evar_map -> rel_context -> rel_context
-val nf_env : evar_map -> env -> env
-
 val combine_params : Names.Idset.t ->
   (Names.Idset.t -> (Names.identifier * bool) option * (Names.identifier * Term.constr option * Term.types) ->
     Topconstr.constr_expr * Names.Idset.t) ->
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index d653ed9466..62bb7ef26d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -56,6 +56,17 @@ 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_named_context_evar sigma ctx = 
+  Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+
+let nf_rel_context_evar sigma ctx = 
+  Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+    
+let nf_env_evar sigma env = 
+  let nc' = nf_named_context_evar sigma (Environ.named_context env) in
+  let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
+    push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
+
 let nf_evar_info evc info =
   { info with 
     evar_concl = Reductionops.nf_evar evc info.evar_concl;
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 36b674fe5a..5fc4ff8db3 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -134,6 +134,10 @@ val tj_nf_evar :
 val nf_evar_info : evar_map -> evar_info -> evar_info
 val nf_evars : evar_map -> evar_map
 
+val nf_named_context_evar : evar_map -> named_context -> named_context
+val nf_rel_context_evar : evar_map -> rel_context -> rel_context
+val nf_env_evar : evar_map -> env -> env
+
 (* Same for evar defs *)
 val nf_isevar :  evar_defs -> constr -> constr
 val j_nf_isevar :  evar_defs -> unsafe_judgment -> unsafe_judgment