diff options
| author | msozeau | 2008-07-24 17:58:35 +0000 |
|---|---|---|
| committer | msozeau | 2008-07-24 17:58:35 +0000 |
| commit | 44233ae7f65d3f1ff360667b867ef890e17e1e46 (patch) | |
| tree | a113b11b45f854174d27fd42ff60287f801d9d53 /toplevel | |
| parent | e024483cc0425b41d3397e7b4255c595dfa14bd1 (diff) | |
Fix bug #1913, checking for unresolved evars which aren't obligations.
Also check mutuality of fixpoints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.mli | 22 |
1 files changed, 10 insertions, 12 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 5950576167..227152f14f 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -56,18 +56,16 @@ val declare_assumption : identifier located list -> val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit - -val compute_interning_datas : Environ.env -> - 'a list -> - 'b list -> - Term.types list -> - Impargs.manual_explicitation list list -> +val compute_interning_datas : Environ.env -> 'a list -> 'b list -> + Term.types list ->Impargs.manual_explicitation list list -> 'a list * - ('b * - (Names.identifier list * Impargs.implicits_list * - Topconstr.scope_name option list)) + ('b * (Names.identifier list * Impargs.implicits_list * + Topconstr.scope_name option list)) list +val check_mutuality : Environ.env -> definition_object_kind -> + (identifier * types) list -> unit + val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit val declare_mutual_with_eliminations : @@ -87,10 +85,10 @@ type fixpoint_expr = { fix_type : constr_expr } -val recursive_message : Decl_kinds.definition_object_kind -> - int array option -> Names.identifier list -> Pp.std_ppcmds +val recursive_message : definition_object_kind -> + int array option -> identifier list -> Pp.std_ppcmds -val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier -> +val declare_fix : bool -> definition_object_kind -> identifier -> constr -> types -> Impargs.manual_explicitation list -> global_reference val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit |