diff options
| author | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-23 18:25:15 +0200 |
| commit | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (patch) | |
| tree | 7546ab8a3bf1a0e2b5a75028e9efcade1d8d4321 /tactics | |
| parent | 13716dc6561a3379ba130f07ce7ecd1df379475c (diff) | |
Hopefully better names to constructors of internal_flag, as discussed
with Enrico.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e4240cb5cc..af0870bc92 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -320,7 +320,7 @@ let project_hint pri l2r r = Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) in let ctx = Evd.universe_context_set sigma in - let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) let add_hints_iff l2r lc n bl = diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 3c4550a3cf..c64a1226ab 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1896,7 +1896,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in let evd = Evd.empty (*FIXME *) in if Lib.is_modtype () then - let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,poly,(instance,Univ.UContext.empty),None), Decl_kinds.IsAssumption Decl_kinds.Logical) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ad7ff14e6b..b113ed31e9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4450,7 +4450,7 @@ let abstract_subproof id gk tac = let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in |