diff options
| author | herbelin | 2009-11-11 16:03:06 +0000 |
|---|---|---|
| committer | herbelin | 2009-11-11 16:03:06 +0000 |
| commit | e46a343090514c1340d4e5b97384b55b42c9c166 (patch) | |
| tree | afe12355bdb7e823b5881b4a89d54b6753684001 /plugins/subtac | |
| parent | d27a272511939ba80f1b3658be064268ec9ba55e (diff) | |
Added support for multiple where-clauses in Inductive and co (see wish #2163).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/subtac')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 007013d405..b61299a068 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -431,7 +431,7 @@ let interp_recursive fixkind l boxed = (* Get interpretation metadatas *) let impls = Constrintern.compute_full_internalization_env env Constrintern.Recursive [] fixnames fixtypes fiximps in - let notations = List.fold_right Option.List.cons ntnl [] in + let notations = List.flatten ntnl in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index c9064ec822..71c93266d1 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -54,7 +54,7 @@ val build_wellfounded : Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress val build_recursive : - (fixpoint_expr * decl_notation option) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> bool -> unit val build_corecursive : - (cofixpoint_expr * decl_notation option) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> bool -> unit |