Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en interp_constr etc.

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

2 files changed, 24 insertions, 26 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 29d02b0138..f7b1c51cc6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -457,7 +457,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 *)
 
 
-let unsafe_fmachine vtcon nocheck isevars metamap env constr = 
+let unsafe_fmachine vtcon nocheck isevars metamap env constr =
   trad_metamap := metamap;
   trad_nocheck := nocheck;
   reset_problems ();
@@ -499,26 +499,24 @@ let ise_resolve fail_evar sigma metamap env c =
   let j = unsafe_fmachine empty_tycon false isevars metamap env c in
   j_apply (fun _ -> process_evars fail_evar) env !isevars j
 
-
 let ise_resolve_type fail_evar sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine def_vty_con false isevars metamap env c in
   let tj = inh_ass_of_j env isevars j in
   typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj
 
-
 let ise_resolve_nocheck sigma metamap env c =
   let isevars = ref sigma in
   let j = unsafe_fmachine empty_tycon true isevars metamap env c in
   j_apply (fun _ -> process_evars true) env !isevars j
 
-
 let ise_resolve1 is_ass sigma env c =
   if is_ass then 
     body_of_type (ise_resolve_type true sigma [] env c)
   else 
     (ise_resolve true sigma [] env c).uj_val
 
+
 (* Keeping universe constraints *)
 (*
 let fconstruct_type_with_univ_sp sigma sign sp c =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c4af6472d3..a20b1eb3f4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -11,6 +11,25 @@ open Rawterm
 open Evarutil
 (*i*)
 
+(* Raw calls to the inference machine of Trad: boolean says if we must fail
+ * on unresolved evars, or replace them by Metas *)
+val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> unsafe_judgment
+val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> typed_type
+
+(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
+ * if we must coerce to a type *)
+val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
+
+val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
+
+(* progmach.ml tries to type ill-typed terms: does not perform the conversion
+ * test in application.
+ *)
+val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
+  env -> rawconstr -> unsafe_judgment
+
 (* Typing with Trad, and re-checking with Mach *)
 (*i
 val infconstruct_type :
@@ -36,30 +55,11 @@ val infconstruct_type_with_univ_sp :
   -> Impuniv.universes * (typed_type * information)
 i*)
 
-(* Low level typing functions, for terms with de Bruijn indices and Metas *)
-
-(* Raw calls to the inference machine of Trad: boolean says if we must fail
- * on unresolved evars, or replace them by Metas *)
-val ise_resolve : bool -> 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> unsafe_judgment
-val ise_resolve_type : bool -> 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> typed_type
-
-(* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says
- * if we must coerce to a type *)
-val ise_resolve1 : bool -> 'a evar_map -> env -> rawconstr -> constr
-
-val ise_resolve_casted : 'a evar_map -> env -> constr -> rawconstr -> constr
-
-(* progmach.ml tries to type ill-typed terms: does not perform the conversion
- * test in application.
- *)
-val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
-  env -> rawconstr -> unsafe_judgment
-
-
+(*i*)
 (* Internal of Trad...
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
   trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment
+
+(*i*)