diff options
| -rw-r--r-- | tactics/declare.ml | 3 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 4 | ||||
| -rw-r--r-- | vernac/comAssumption.mli | 2 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 2 |
5 files changed, 6 insertions, 7 deletions
diff --git a/tactics/declare.ml b/tactics/declare.ml index cdbb3d41d9..17e873f017 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -300,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -317,7 +317,6 @@ let declare_variable ~name ~kind d = | SectionLocalAssum {typ;univs;poly;impl} -> let () = declare_universe_context ~poly univs in let () = Global.push_named_assum (name,typ) in - let impl = if impl then Glob_term.Implicit else Glob_term.Explicit in impl, true, poly | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a diff --git a/tactics/declare.mli b/tactics/declare.mli index 89b41076f7..4ae9f6c7ae 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = | DefinitionEntry of 'a Proof_global.proof_entry diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 7d365db85c..e3f90ab98c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -100,7 +100,7 @@ let next_uctx = let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = let refs, _ = List.fold_left (fun (refs,uctx) id -> - let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in + let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in ref::refs, next_uctx uctx) ([],uctx) idl in @@ -292,7 +292,7 @@ let context ~poly l = | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = List.exists test impls in + let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in let scope = if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in match b with diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 1632c3d578..2715bd8305 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -34,7 +34,7 @@ val declare_assumption -> Entries.universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits - -> bool (** implicit *) + -> Glob_term.binding_kind -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index adfb058942..7809425a10 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -258,7 +258,7 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = false in (* copy values from Vernacentries *) + let impl = Glob_term.Explicit in let univs = match univs with | Polymorphic_entry (_, univs) -> (* What is going on here? *) |