diff options
| author | Pierre-Marie Pédrot | 2019-06-08 16:50:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:08 +0200 |
| commit | 929ecfe0cd8cd3edec41416491e286e4c105ffa6 (patch) | |
| tree | 74acaf09aae9dec751c430e4c8bb0127b06cc363 /tactics | |
| parent | e753855167e5629775b604128c6efc9d58ee626c (diff) | |
Move the side-effect role out of Entries into Evd.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 4 |
2 files changed, 3 insertions, 3 deletions
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 |