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/comAssumption.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/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a0b0dcf4c8..e5db6146ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -69,7 +69,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in + let () = DeclareUniv.declare_univ_binders gr pl in let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in |