diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /toplevel/command.mli | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'toplevel/command.mli')
-rw-r--r-- | toplevel/command.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index c93f69be..6f9a55c3 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command.mli 7682 2005-12-21 15:06:11Z herbelin $ i*) +(*i $Id: command.mli 9110 2006-09-01 12:30:52Z herbelin $ i*) (*i*) open Util @@ -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 |