diff options
| author | Emilio Jesus Gallego Arias | 2020-06-03 16:34:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-03 17:33:25 +0200 |
| commit | 6fe12fdac4acee36c99ea780d260ce5a9756cb1d (patch) | |
| tree | 9e3016023ed13df51988a84e6f1f8b26d4b0584d /vernac/declare.ml | |
| parent | 5ea6ef71681770a98edc5ede8614d2cf0bd48554 (diff) | |
[declare] Hide internals of variable declaration entries.
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
Diffstat (limited to 'vernac/declare.ml')
| -rw-r--r-- | vernac/declare.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 -> |