diff options
| author | Gaëtan Gilbert | 2018-08-23 10:59:29 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 14:03:04 +0200 |
| commit | b3577d942307c3a23aabd224a588af16a0337094 (patch) | |
| tree | 5529d92eed92dddb1129db6354a59e5b8cd135e2 | |
| parent | e8937bfe903c7acbdfaa9d65bc0f5aaaa74a2bae (diff) | |
Elaboration: do not ask poly inductives to be template
| -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 0ca1bfd0c0..d23784f774 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -423,7 +423,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) -> { mind_entry_typename = ind.ind_name; mind_entry_arity = arity; - mind_entry_template = Option.cata (fun s -> not (Sorts.is_small s)) false concl; + mind_entry_template = not poly && Option.cata (fun s -> not (Sorts.is_small s)) false concl; mind_entry_consnames = cnames; mind_entry_lc = ctypes }) indl arities arityconcl constructors in |