diff options
| author | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
| commit | 028d64fb5c461e32752b0f8a92d4e2eca2a26d0d (patch) | |
| tree | 8380a901d2c066536f38552f67ffa76f0e3364b3 /vernac/comInductive.ml | |
| parent | 3b9763487f96d308f6339c7eb4fc834b069f6e40 (diff) | |
| parent | cc3ded87f0f440eac2746d59b7aeba60ca9f691f (diff) | |
Merge PR #11293: Rename files with Class in their name to make their role clearer.
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b603c54026..8de1c69424 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -553,7 +553,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni (* 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 (Nametab.locate qid) ~local:false ~poly) coes + List.iter (fun qid -> ComCoercion.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name |