From 8bc5a17d7beb67a68befe2fcd73932d477d1925f Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 24 Apr 2009 09:29:08 +0000 Subject: - 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 --- plugins/subtac/subtac_command.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/subtac/subtac_command.ml') 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 -- cgit v1.2.3