forked from mattam82/Coq-Equations
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathderive.mli
25 lines (20 loc) · 1.3 KB
/
derive.mli
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(**********************************************************************)
(* Equations *)
(* Copyright (c) 2009-2016 Matthieu Sozeau <matthieu.sozeau@inria.fr> *)
(**********************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(**********************************************************************)
type derive_record =
{ derive_name : string;
derive_fn : polymorphic:Decl_kinds.polymorphic -> Globnames.global_reference -> unit }
(** When the Derive expects a constr. *)
val make_derive :
(Environ.env -> Evd.evar_map -> polymorphic:Decl_kinds.polymorphic -> EConstr.constr -> unit) ->
polymorphic:bool -> Globnames.global_reference -> unit
(** When the Derive works on inductive types only. *)
val make_derive_ind :
(Environ.env -> Evd.evar_map -> polymorphic:Decl_kinds.polymorphic -> Names.inductive * EConstr.EInstance.t -> unit) ->
polymorphic:bool -> Globnames.global_reference -> unit
val register_derive : derive_record -> unit
val derive : poly:bool -> string list -> Globnames.global_reference Loc.located list -> unit