diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-26 21:15:36 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:40:10 +0200 |
| commit | e0547f9e9134a9fff122df900942a094c53535c3 (patch) | |
| tree | 9b5a11a7fb28857dd26f472d6329e14a1529393a /toplevel/command.mli | |
| parent | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (diff) | |
Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness.
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 3ec65b487..7112591fe 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -146,12 +146,14 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : + chkguard:bool -> locality -> polymorphic -> recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit -val declare_cofixpoint : locality -> polymorphic -> +val declare_cofixpoint : + chkguard:bool -> locality -> polymorphic -> recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -159,9 +161,11 @@ val declare_cofixpoint : locality -> polymorphic -> (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : + chkguard:bool -> (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : + chkguard:bool -> (* When [false], assume guarded. *) locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) |