- New cleaning phase for the entry points of pretyping.ml

- Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml 
  so as to ease the comparison between these files. Application of a
  change that cannot do harm: j_nf_evar now called after getting evd
  from consider_remaining_unif_problems in
  Subtac_pretyping_F.understand_judgment. Four differences remain
  (is it the sign of a problem?):
  1) understand_type fails in Pretyping if evars remain but does not fail in
     Subtac_pretyping_F
  2) resolve_typeclasses (when called) is called with ~onlyargs:false and 
     ~fail:true in Pretyping.understand, Pretyping.understand_gen and
     Pretyping.understand_type but with true and false in these same
     functions in Subtac_pretyping_F
  3) understand_ltac does not call typeclasses in Pretyping but it
     does call it in Subtac_pretyping_F
  4) understand_judgment does call typeclasses in Pretyping but not in
     Subtac_pretyping_F



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

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 0bfafa492f..6ffb36e411 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -58,7 +58,7 @@ let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
-  let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
+  let c' = SPretyping.understand_tcc_evars isevars env kind c' in
     evar_nf isevars c'
 
 let interp_constr isevars env c =
@@ -76,7 +76,7 @@ let interp_casted_constr_evars isevars env ?(impls=([],[])) c typ =
 let interp_open_constr isevars env c =
     msgnl (str "Pretyping " ++ my_print_constr_expr c);
   let c = Constrintern.intern_constr ( !isevars) env c in
-  let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
+  let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in
     evar_nf isevars c'
 
 let interp_constr_judgment isevars env c =
@@ -96,7 +96,7 @@ let locate_if_isevar loc na = function
 
 let interp_binder sigma env na t =
   let t = Constrintern.intern_gen true ( !sigma) env t in
-    SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)
 
 let interp_context_evars evdref env params = 
   let bl = Constrintern.intern_context false ( !evdref) env params in