diff options
| author | msozeau | 2008-03-24 12:06:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-24 12:06:12 +0000 |
| commit | 467fb77527b75cf6c214aa3b72b2826cae2e18ae (patch) | |
| tree | 74da515805cfcd0e91d47fa0523d963080650c32 /interp | |
| parent | 20e9bca4d769e3d538e34469c8596e4215fd5f19 (diff) | |
Finish fix in command where we still lost information on what was a type
and needed coercions. Change API of interp_constr_evars to get an
optional evar_defs ref argument. Makes Algebra compile again (at least).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10715 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |