← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to pretyping/typeclasses.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
pretyping/typeclasses.mli
 
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
(************************************************************************)
 
8
 
 
9
(*i $Id: typeclasses.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
10
 
 
11
(*i*)
 
12
open Names
 
13
open Libnames
 
14
open Decl_kinds
 
15
open Term
 
16
open Sign
 
17
open Evd
 
18
open Environ
 
19
open Nametab
 
20
open Mod_subst
 
21
open Topconstr
 
22
open Util
 
23
(*i*)
 
24
 
 
25
(* This module defines type-classes *)
 
26
type typeclass = {
 
27
  (* The class implementation: a record parameterized by the context with defs in it or a definition if 
 
28
     the class is a singleton. This acts as the class' global identifier. *)
 
29
  cl_impl : global_reference; 
 
30
 
 
31
  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. 
 
32
     The boolean indicates if the typeclass argument is a direct superclass and the global reference
 
33
     gives a direct link to the class itself. *)
 
34
  cl_context : (global_reference * bool) option list * rel_context; 
 
35
 
 
36
  (* Context of definitions and properties on defs, will not be shared *)
 
37
  cl_props : rel_context;
 
38
 
 
39
  (* The methods implementations of the typeclass as projections. Some may be undefinable due to 
 
40
     sorting restrictions. *)
 
41
  cl_projs : (identifier * constant option) list;
 
42
}
 
43
 
 
44
type instance
 
45
 
 
46
val instances : global_reference -> instance list
 
47
val typeclasses : unit -> typeclass list
 
48
val all_instances : unit -> instance list
 
49
 
 
50
val add_class : typeclass -> unit
 
51
 
 
52
val new_instance : typeclass -> int option -> bool -> constant -> instance
 
53
val add_instance : instance -> unit
 
54
 
 
55
val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
 
56
 
 
57
 
 
58
(* These raise a UserError if not a class. *)
 
59
val dest_class_app : env -> constr -> typeclass * constr list
 
60
 
 
61
(* Just return None if not a class *)
 
62
val class_of_constr : constr -> typeclass option
 
63
  
 
64
val instance_impl : instance -> constant
 
65
 
 
66
val is_class : global_reference -> bool
 
67
val is_instance : global_reference -> bool
 
68
val is_method : constant -> bool
 
69
 
 
70
val is_implicit_arg : hole_kind -> bool
 
71
 
 
72
(* Returns the term and type for the given instance of the parameters and fields
 
73
   of the type class. *)
 
74
 
 
75
val instance_constructor : typeclass -> constr list -> constr * types
 
76
 
 
77
(* Use evar_extra for marking resolvable evars. *)
 
78
val bool_in : bool -> Dyn.t
 
79
val bool_out : Dyn.t -> bool
 
80
 
 
81
val is_resolvable : evar_info -> bool
 
82
val mark_unresolvable : evar_info -> evar_info
 
83
val mark_unresolvables : evar_map -> evar_map
 
84
val is_class_evar : evar_info -> bool
 
85
 
 
86
val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> 
 
87
  env -> evar_defs -> evar_defs
 
88
val resolve_one_typeclass : env -> evar_map -> types -> constr
 
89
 
 
90
val register_add_instance_hint : (constant -> int option -> unit) -> unit
 
91
val add_instance_hint : constant -> int option -> unit
 
92
 
 
93
val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref
 
94
val solve_instanciation_problem : (env -> evar_map -> types -> constr) ref
 
95