From 929ecfe0cd8cd3edec41416491e286e4c105ffa6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 8 Jun 2019 16:50:32 +0200
Subject: Move the side-effect role out of Entries into Evd.

---
 tactics/abstract.ml   | 2 +-
 tactics/ind_tables.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 0547071519..967b0ef418 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
+    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Entries.const_entry_universes with
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index eaff889dbf..539fe31416 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -145,7 +145,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let role = Entries.Schema (ind, kind) in
+  let role = Evd.Schema (ind, kind) in
   let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
   const, Evd.concat_side_effects neff eff
@@ -163,7 +163,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let fold i effs id cl =
-    let role = Entries.Schema ((mind, i), kind)in
+    let role = Evd.Schema ((mind, i), kind)in
     let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in
     (Evd.concat_side_effects neff effs, cst)
   in
-- 
cgit v1.2.3