diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 15 | ||||
| -rw-r--r-- | interp/constrintern.mli | 7 |
2 files changed, 15 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 49b719bdb5..ee245450b4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1187,7 +1187,8 @@ let interp_open_constr sigma env c = let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) -let interp_constr_evars_gen_impls evdref env ?(impls=([],[])) kind c = +let interp_constr_evars_gen_impls ?(evdref=ref Evd.empty_evar_defs) + env ?(impls=([],[])) kind c = let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in let imps = implicits_of_rawterm c in Default.understand_tcc_evars evdref env kind c, imps @@ -1196,11 +1197,15 @@ let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = let c = intern_gen (kind=IsType) ~impls (Evd.evars_of !evdref) env c in Default.understand_tcc_evars evdref env kind c -let interp_casted_constr_evars_impls evdref env ?(impls=([],[])) c typ = - interp_constr_evars_gen_impls evdref env ~impls (OfType (Some typ)) c +let interp_casted_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs) + env ?(impls=([],[])) c typ = + interp_constr_evars_gen_impls ~evdref env ~impls (OfType (Some typ)) c -let interp_type_evars_impls evdref env ?(impls=([],[])) c = - interp_constr_evars_gen_impls evdref env IsType ~impls c +let interp_type_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c = + interp_constr_evars_gen_impls ~evdref env IsType ~impls c + +let interp_constr_evars_impls ?(evdref=ref Evd.empty_evar_defs) env ?(impls=([],[])) c = + interp_constr_evars_gen_impls ~evdref env (OfType None) ~impls c let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 9f3a815ee0..f81b2ccd16 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -86,12 +86,15 @@ val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env -> (* Accepting evars and giving back the manual implicits in addition. *) -val interp_casted_constr_evars_impls : evar_defs ref -> env -> +val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits -val interp_type_evars_impls : evar_defs ref -> env -> ?impls:full_implicits_env -> +val interp_type_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env -> constr_expr -> types * manual_implicits +val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> env -> ?impls:full_implicits_env -> + constr_expr -> constr * manual_implicits + val interp_casted_constr_evars : evar_defs ref -> env -> ?impls:full_implicits_env -> constr_expr -> types -> constr |