From bd21ec85ff71e49b12d48e4ed3bf72a3f48a60d2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 May 2019 02:12:01 +0200
Subject: Ensure dynamically that opaque definitions come with their type.

The only lawbreaker was the Add Ring command. We generate a type for
the declaration to fix the code.
---
 plugins/setoid_ring/newring.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index aeceeb4e50..8e7b045b8e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,9 +153,11 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let univs = Monomorphic_entry univs in
+  let () = Declare.declare_universe_context 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 ~univs c),
+            (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
 	     IsProof Lemma))
 
 (* Calling a global tactic *)
-- 
cgit v1.2.3