diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 20:01:04 +0000 |
| commit | 0601db38b579513e4ab39a161591cd359260490e (patch) | |
| tree | 2741c3b805ec8b890c5b9f58aeb1445ec10590fc /interp/constrintern.mli | |
| parent | 8556f4e4b5e21535013e6962feabfede6313462b (diff) | |
Promote evar_defs to evar_map (in Evd)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ee677e80a..0e66dde83 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -117,21 +117,21 @@ val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> (* Accepting evars and giving back the manual implicits in addition. *) -val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> +val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits -val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> +val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> types * manual_implicits -val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> +val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> constr * manual_implicits -val interp_casted_constr_evars : evar_defs ref -> env -> +val interp_casted_constr_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env -> +val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -154,7 +154,7 @@ val interp_reference : ltac_sign -> reference -> rawconstr val interp_binder : evar_map -> env -> name -> constr_expr -> types -val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types +val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types (* Interpret contexts: returns extended env and context *) @@ -162,7 +162,7 @@ val interp_context : ?fail_anonymous:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits val interp_context_evars : ?fail_anonymous:bool -> - evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) (* (these functions do not modify the glob file) *) |