diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/classes.ml | 5 | ||||
-rw-r--r-- | toplevel/command.ml | 10 | ||||
-rw-r--r-- | toplevel/command.mli | 4 |
3 files changed, 13 insertions, 6 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 915ab9d4c..640bd0b08 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -343,6 +343,9 @@ let context l = in let impl = List.exists test impls in let decl = (Discharge, Definitional) in - let nstatus = Command.declare_assumption false decl t [] impl None (Loc.ghost, id) in + let nstatus = + Command.declare_assumption false decl t [] impl + Vernacexpr.NoInline (Loc.ghost, id) + in status && nstatus in List.fold_left fn true (List.rev ctx) diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b2e6b352..f8230d63d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -34,6 +34,7 @@ open Evarutil open Evarconv open Indschemes open Misctypes +open Vernacexpr let rec under_binders env f n c = if Int.equal n 0 then f env Evd.empty c else @@ -188,7 +189,12 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca true | Global | Local | Discharge -> let local = get_locality ident local in - let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in + let inl = match nl with + | NoInline -> None + | DefaultInline -> Some (Flags.get_inline_level()) + | InlineAt i -> Some i + in + let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in let kn = declare_constant ident ~local decl in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -386,8 +392,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls = declare_default_schemes mind; mind -open Vernacexpr - type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) diff --git a/toplevel/command.mli b/toplevel/command.mli index eb0eef38f..08151c859 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -51,11 +51,11 @@ val interp_assumption : nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool (** implicit *) -> Entries.inline -> variable Loc.located -> bool + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> bool val declare_assumptions : variable Loc.located list -> coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool -> Entries.inline -> bool + bool -> Vernacexpr.inline -> bool (** {6 Inductive and coinductive types} *) |