diff options
| author | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 16:46:25 +0200 |
| commit | cddd0149b686b247116681a17b5c7bf42d513115 (patch) | |
| tree | f8696c9ad900efd1b54bd9ca84daddf12fdb580f /plugins/setoid_ring | |
| parent | 48f73e492465f3c46438583c069bc0ba745ef56f (diff) | |
| parent | 8de0fcaa08c82ece8874606e8fa1954d860bd88e (diff) | |
Merge PR #12130: [declare] [tactics] Move declare to `vernac`
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0646af3552..633cdbd735 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -150,7 +150,7 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in - let () = Declare.declare_universe_context ~poly:false univs in + let () = DeclareUctx.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 ~name:(Id.of_string na) |