blob: f25abb95c36c5b091772607dbcf809d7a3756117 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
open Vernacexpr
(** Special Fixpoint handling when command is activated. *)
val do_fixpoint :
(* When [false], assume guarded. *)
scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint :
(* When [false], assume guarded. *)
scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
|
