diff options
| author | Gaëtan Gilbert | 2017-09-18 17:22:24 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-24 19:23:41 +0100 |
| commit | 34d85e1e899f8a045659ccc53bfd6a1f5104130b (patch) | |
| tree | ed176f6f7d0d47802d5c4e1879cd2eb35232df46 /plugins/ltac | |
| parent | 58c0784745f8b2ba7523f246c4611d780c9f3f70 (diff) | |
Use Entries.constant_universes_entry more.
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 6 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 9 |
2 files changed, 6 insertions, 9 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d6cfa3cf9a..750517e91a 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -313,10 +313,10 @@ let project_hint pri l2r r = let id = 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 = EConstr.to_constr sigma c in let poly = Flags.use_polymorphic_flag () in - let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c)) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a2f5a4577f..c0060c5a7c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1884,11 +1884,11 @@ let declare_projection n instance_id r = in it_mkProd_or_LetIn ccl ctx in let typ = it_mkProd_or_LetIn typ ctx in - let ctx = Evd.to_universe_context sigma in + let univs = Evd.const_univ_entry ~poly sigma in let typ = EConstr.to_constr sigma typ in let term = EConstr.to_constr sigma term in let cst = - Declare.definition_entry ~types:typ ~poly ~univs:ctx term + Declare.definition_entry ~types:typ ~univs term in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) @@ -1972,10 +1972,7 @@ let add_morphism_infer glob m n = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in if Lib.is_modtype () then - let uctx = if poly - then Entries.Polymorphic_const_entry (UState.context uctx) - else Entries.Monomorphic_const_entry (UState.context_set uctx) - in + let uctx = UState.const_univ_entry ~poly uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry (None,(instance,uctx),None), |