diff options
| author | msozeau | 2008-02-08 16:42:26 +0000 |
|---|---|---|
| committer | msozeau | 2008-02-08 16:42:26 +0000 |
| commit | c164dc2aadd8d26b362669b9af6b45cbd8e563ff (patch) | |
| tree | beb528d5a47d69ef81c52f9ddbef17cde7fb9e26 /toplevel | |
| parent | 14eb998277c1639a02139023a642ee680f6c6a79 (diff) | |
Backport code from command.ml to subtac_command.ml for definining
recursive definitions. Now program accepts cofixpoints and uses the new
way infer structurally decreasing arguments. Also, checks for correct
recursive calls before giving the definition to the obligations machine
(solves part 1 of bug #1784).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.mli | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 6b15479d77..d587fabf77 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -43,6 +43,10 @@ val declare_assumption : identifier located list -> coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool ->unit +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 -> @@ -58,9 +62,26 @@ 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 +type fixpoint_kind = + | IsFixpoint of (int option * recursion_order_expr) list + | IsCoFixpoint + +type fixpoint_expr = { + fix_name : identifier; + fix_binders : local_binder list; + fix_body : constr_expr; + fix_type : constr_expr +} + +val recursive_message : Decl_kinds.definition_object_kind -> + int array option -> Names.identifier list -> Pp.std_ppcmds + +val declare_fix : bool -> Decl_kinds.definition_object_kind -> identifier -> + constr -> types -> Impargs.manual_explicitation list -> global_reference + +val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit -val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit +val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit val build_scheme : (identifier located option * scheme ) list -> unit |