diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:56:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | 0bc7e7405553dc63d9693e85c3ce1485b5e8fe23 (patch) | |
| tree | 29a75b9b4edf5e20e939ab9c5779c5516294517d /plugins/setoid_ring | |
| parent | fa1782e05eeb6f18871d26cc43670d35ed73bf23 (diff) | |
[declare] Separate kinds from entries in constant declaration
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 3d6bfda0b2..9973f2ec1d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -155,9 +155,9 @@ let decl_constant na univs c = let () = Declare.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in - mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), - Decls.(IsProof Lemma))) + mkConst(declare_constant ~name:(Id.of_string na) + ~kind:Decls.(IsProof Lemma) + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c))) (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = |