diff options
| -rw-r--r-- | vernac/comAssumption.ml | 3 | ||||
| -rw-r--r-- | vernac/declare.ml | 7 | ||||
| -rw-r--r-- | vernac/declare.mli | 10 |
3 files changed, 8 insertions, 12 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 023d76ce3b..44c30598aa 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -24,8 +24,7 @@ module RelDecl = Context.Rel.Declaration let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let kind = Decls.IsAssumption kind in - let decl = Declare.SectionLocalAssum {typ; impl} in - let () = Declare.declare_variable ~name ~kind decl in + let () = Declare.declare_variable ~name ~kind ~typ ~impl in let () = Declare.assumption_message name in let r = GlobRef.VarRef name in let () = maybe_declare_manual_implicits true r imps in diff --git a/vernac/declare.ml b/vernac/declare.ml index 6ed7a9e39d..7de1ff4083 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -554,7 +554,7 @@ let objVariable : unit Libobject.Dyn.tag = let inVariable v = Libobject.Dyn.Easy.inj v objVariable -let declare_variable ~name ~kind d = +let declare_variable_core ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then raise (DeclareUniv.AlreadyDeclared (None, name)); @@ -591,6 +591,9 @@ let declare_variable ~name ~kind d = Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) +let declare_variable ~name ~kind ~typ ~impl = + declare_variable_core ~name ~kind (SectionLocalAssum { typ; impl }) + (* Declaration messages *) let pr_rank i = pr_nth (i+1) @@ -913,7 +916,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry = let ubind = UState.universe_binders uctx in let dref = match scope with | Discharge -> - let () = declare_variable ~name ~kind (SectionLocalDef entry) in + let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name | Global local -> diff --git a/vernac/declare.mli b/vernac/declare.mli index 5339f4702b..ef4f8c4825 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -119,13 +119,6 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t (** XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead *) -type variable_declaration = - | SectionLocalDef of Evd.side_effects proof_entry - | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; } - -(** XXX: This is an internal, low-level API and could become scheduled - for removal from the public API, use higher-level declare APIs - instead *) type 'a constant_entry = | DefinitionEntry of 'a proof_entry | ParameterEntry of parameter_entry @@ -134,7 +127,8 @@ type 'a constant_entry = val declare_variable : name:variable -> kind:Decls.logical_kind - -> variable_declaration + -> typ:types + -> impl:Glob_term.binding_kind -> unit (** Declaration of global constructions |