diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 33b22c3b73..f56a924756 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -292,7 +292,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty) = match kind_of_term f with - | (Ind _ | Const _) + | (Ind _ (* needed if defs in Type are polymorphic: | Const _*)) when not (array_exists occur_meta l) (* we could be finer *) -> (* Sort-polymorphism of definition and inductive types *) goalacc, |