diff options
author | 2012-03-14 09:52:25 +0000 | |
---|---|---|
committer | 2012-03-14 09:52:25 +0000 | |
commit | 1b3efc6dc25be1bfde5fb7d2d39cc5c35e44a4d8 (patch) | |
tree | 3f22240472bd260847f4b5b26581cfdfbc3e071a /plugins/subtac/subtac_classes.ml | |
parent | 1674ab8bc0b76a1162928d0d9097c6a97486205d (diff) |
Second step of integration of Program:
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac/subtac_classes.ml')
-rw-r--r-- | plugins/subtac/subtac_classes.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index a81243f73..75d0f3429 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -25,10 +25,8 @@ open Entries open Errors open Util -module SPretyping = Subtac_pretyping.Pretyping - let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = - SPretyping.understand_tcc_evars evdref env kind + understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls !evdref env c) let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = @@ -36,13 +34,13 @@ let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internaliza let interp_context_evars evdref env params = let impls_env, bl = Constrintern.interp_context_gen - (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t) - (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl + (fun env t -> understand_tcc_evars evdref env IsType t) + (understand_judgment_tcc evdref) !evdref env params in bl let interp_type_evars_impls ~evdref ?(impls=empty_internalization_env) env c = let c = intern_gen true ~impls !evdref env c in let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in - SPretyping.understand_tcc_evars ~fail_evar:false evdref env IsType c, imps + understand_tcc_evars ~fail_evar:false evdref env IsType c, imps let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function |