diff options
| author | Gaëtan Gilbert | 2019-10-28 15:14:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-28 15:14:20 +0100 |
| commit | 42eac2b1cee72acce4ebf0ce3e74dd60763b223b (patch) | |
| tree | 64c52c4fba7b2432797ad940765b5f74c4c10952 /vernac/classes.ml | |
| parent | 9297352202fa6a43faf266a97a6a07d1df317b9a (diff) | |
| parent | bd27f8b3c9894a73f3f93662f6ff11dfb8fb65c4 (diff) | |
Merge PR #10950: [declare] Split universe and inductive declaration code to vernac/
Ack-by: Janno
Reviewed-by: SkySkimmer
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 702a3e44a9..09866a75c9 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -325,7 +325,7 @@ let declare_instance_constant info global imps ?hook name decl poly sigma term t let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; - Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = @@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in - Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (GlobRef.ConstRef cst) let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = |