diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
-rw-r--r-- | vernac/comDefinition.mli | 4 | ||||
-rw-r--r-- | vernac/comFixpoint.ml | 1 | ||||
-rw-r--r-- | vernac/comFixpoint.mli | 2 | ||||
-rw-r--r-- | vernac/comInductive.ml | 2 | ||||
-rw-r--r-- | vernac/comInductive.mli | 2 |
6 files changed, 6 insertions, 7 deletions
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 0491638c9..eaa114661 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 4a65c1e91..2e6ee885c 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,7 +15,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> - Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -25,6 +25,6 @@ val do_definition : program_mode:bool -> (** Not used anywhere. *) val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Univdecls.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index edfe7aa81..a794c2db0 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -14,7 +14,6 @@ open Pretyping open Evarutil open Evarconv open Misctypes -open Vernacexpr module RelDecl = Context.Rel.Declaration diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 2926e30e5..9bb49d5de 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -30,7 +30,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; + fix_univs : Constrexpr.universe_decl_expr option; fix_annot : Misctypes.lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index cef5546c6..fce263bdb 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -55,7 +55,7 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 82ea131e1..c978a963f 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -45,7 +45,7 @@ val declare_mutual_inductive_with_eliminations : type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } |