diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 33798c43c8..9973f2ec1d 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -29,7 +29,6 @@ open Tacinterp open Libobject open Printer open Declare -open Decl_kinds open Entries open Newring_ast open Proofview.Notations @@ -156,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), - 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) = |