diff options
| author | Arnaud Spiwack | 2014-09-03 18:40:49 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | a54aefa7d2296ef3908dc21087c27250387819cc (patch) | |
| tree | 77a078a0daab703ca4e7fc6fa8010e7531107af7 | |
| parent | 3c29ea3b2e58a7f76195834e9ab43d7e99a0a323 (diff) | |
Commands like [Inductive > X := … | … | …] raise an error message instead of silently ignoring the ">" syntax.
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index adfccb5023..b8baca9eb0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -556,7 +556,9 @@ let vernac_inductive poly lo finite indl = | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> Errors.error "where clause not supported for (co)inductive records" | _ -> let unpack = function - | ( (_, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn + | ( (false, id) , bl , c , _ , Constructors l ) , ntn -> ( id , bl , c , l ) , ntn + | ( (true,_),_,_,_,Constructors _),_ -> + Errors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead." | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in |