blob: 943cb8efe6770bd9b6a2443e607461d647173faa (
plain)
1
2
3
4
5
6
7
8
9
10
11
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
|