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/constrintern.ml | |
| 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/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 15 |
1 files changed, 10 insertions, 5 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 |