diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:38:18 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:38:18 +0100 |
| commit | 3da76841125ef48889c8eceb134116e2d0bd7a2e (patch) | |
| tree | 8728b456dab71560379044459e7a7c979a1b252b /vernac/comProgramFixpoint.mli | |
| parent | 0168ee0b6463a9ef44d768b0020b34785986c1cb (diff) | |
| parent | 1172b52735a299dfc91aee36b30b576dfeff581c (diff) | |
Merge PR #6419: [vernac] Split `command.ml` into separate files.
Diffstat (limited to 'vernac/comProgramFixpoint.mli')
| -rw-r--r-- | vernac/comProgramFixpoint.mli | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli new file mode 100644 index 000000000..943cb8efe --- /dev/null +++ b/vernac/comProgramFixpoint.mli @@ -0,0 +1,12 @@ +open Decl_kinds +open Vernacexpr + +(** Special Fixpoint handling when command is activated. *) + +val do_fixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + +val do_cofixpoint : + (* When [false], assume guarded. *) + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit |