aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comProgramFixpoint.mli
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