diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-17 15:01:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-17 15:01:24 +0000 |
| commit | 5b318ca418ef27d1bf2b155bebbf2425f65b4f1f (patch) | |
| tree | b04fb45d1fd3e8fb6b4253a2acbd595754ec7dc6 /toplevel/vernacexpr.ml | |
| parent | 95f8a0ac38cbd792a0b5d8006aac1ef1a9f70da8 (diff) | |
Ajout "at next level" dans Notation
Mise en place structure pour définir un objet en même temps que sa notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 99ce8b34e..b2f82854c 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -122,11 +122,13 @@ type inductive_flag = bool (* true = Inductive; false = CoInductive *) type sort_expr = Rawterm.rawsort +type decl_notation = (string * scope_name option) option type simple_binder = identifier * constr_expr type 'a with_coercion = coercion_flag * 'a type constructor_expr = simple_binder with_coercion type inductive_expr = - identifier * simple_binder list * constr_expr * constructor_expr list + identifier * decl_notation * simple_binder list * constr_expr + * constructor_expr list type definition_expr = | ProveBody of local_binder list * constr_expr | DefineBody of local_binder list * raw_red_expr option * constr_expr |