diff options
| author | Maxime Dénès | 2017-09-15 10:00:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-15 10:00:35 +0200 |
| commit | 6c678a68c081ce24bbdcb092db3f57ef7e171dac (patch) | |
| tree | d963048adb529427abc19d49f453f276b720df7d /vernac | |
| parent | eb439843c5fd3841aa22b36453c49d9dd07bd770 (diff) | |
| parent | 49f144daf071dcb4e06be54315bd1e92dbe64d68 (diff) | |
Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" Inductive-keyworded record failing even on non-dependent goal)
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 2be10a0397..e15911dd65 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1176,7 +1176,7 @@ let error_not_allowed_case_analysis isrec kind i = pr_inductive (Global.env()) (fst i) ++ str "." let error_not_allowed_dependent_analysis isrec i = - str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + str "Dependent " ++ str (if isrec then "induction" else "case analysis") ++ strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) i ++ str "." |