diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-18 18:05:56 +0000 |
| commit | 6946bbbf2390024b3ded7654814104e709cce755 (patch) | |
| tree | 643429de27ef09026b937c18a55075eb49b11fee /checker/declarations.mli | |
| parent | aa37087b8e7151ea96321a11012c1064210ef4ea (diff) | |
Modulification of mod_bound_id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/declarations.mli')
| -rw-r--r-- | checker/declarations.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/declarations.mli b/checker/declarations.mli index c14d8b73a..ad234a3f5 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -185,7 +185,7 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body + | SEBfunctor of MBId.t * module_type_body * struct_expr_body | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body @@ -215,9 +215,9 @@ and module_type_body = type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_mbid : mod_bound_id -> module_path -> substitution -> substitution +val add_mbid : MBId.t -> module_path -> substitution -> substitution val add_mp : module_path -> module_path -> substitution -> substitution -val map_mbid : mod_bound_id -> module_path -> substitution +val map_mbid : MBId.t -> module_path -> substitution val map_mp : module_path -> module_path -> substitution val mp_in_delta : module_path -> delta_resolver -> bool val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive |