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

1 files changed, 2 insertions, 4 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 =