diff options
| author | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-19 23:34:24 +0200 |
| commit | 02f7b4ac1968ca4522d144e34b52dead3871a8b7 (patch) | |
| tree | 1e649e34972959b77eeebd4c5c6237fd12af1f61 /vernac/comInductive.ml | |
| parent | 3799939088b5aa616974a0d37de7e2616024f222 (diff) | |
| parent | 4ac1e342fe420e0b3f3adc9e619d2e98eba2111d (diff) | |
Merge PR #8758: [api] Qualify access to `Nametab`
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..885a22b209 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () |