1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: classes.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
23
open Implicit_quantifiers
28
val mismatched_params : env -> constr_expr list -> rel_context -> 'a
30
val mismatched_props : env -> constr_expr list -> rel_context -> 'a
32
(* Instance declaration *)
34
val declare_instance : bool -> identifier located -> unit
36
val declare_instance_constant :
38
int option -> (* priority *)
39
bool -> (* globality *)
40
Impargs.manual_explicitation list -> (* implicits *)
41
?hook:(Names.constant -> unit) ->
42
identifier -> (* name *)
43
Term.constr -> (* body *)
44
Term.types -> (* type *)
48
?global:bool -> (* Not global by default. *)
50
typeclass_constraint ->
53
?tac:Proof_type.tactic ->
54
?hook:(constant -> unit) ->
58
(* For generation on names based on classes only *)
60
val id_of_class : typeclass -> identifier
64
val context : ?hook:(Libnames.global_reference -> unit) ->
65
local_binder list -> unit
67
(* Forward ref for refine *)
69
val refine_ref : (open_constr -> Proof_type.tactic) ref