diff options
| author | herbelin | 2006-09-01 12:30:52 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-01 12:30:52 +0000 |
| commit | 5a87d97bd8bce29d3c94bd40e4ab03c4c7c098a8 (patch) | |
| tree | 3ad8750efcbc0bea1c4fc2dcbb57251391bf8a93 /toplevel/command.mli | |
| parent | bd358a1f07807970bebf73f14f0ec941e34d9737 (diff) | |
Ajout possibilité clause "where" dans co-points fixes
(+ uniformisation position notation dans les blocs inductifs et récursifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index be589da1a3..7c3d519469 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -39,14 +39,14 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit -val build_mutual : inductive_expr list -> bool -> unit +val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : bool -> Entries.mutual_inductive_entry -> mutual_inductive val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit -val build_corecursive : cofixpoint_expr list -> bool -> unit +val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located * bool * reference * rawsort) list -> unit |