summaryrefslogtreecommitdiff
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /pretyping/recordops.mli
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'pretyping/recordops.mli')
-rw-r--r--pretyping/recordops.mli46
1 files changed, 24 insertions, 22 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index b71c4969..6165fac2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,23 +1,22 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: recordops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
open Names
open Nametab
open Term
open Libnames
open Libobject
open Library
-(*i*)
-(*s A structure S is a non recursive inductive type with a single
+(** Operations concerning records and canonical structures *)
+
+(** {6 Records } *)
+(** A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
type struc_typ = {
@@ -26,37 +25,40 @@ type struc_typ = {
s_PROJKIND : (name * bool) list;
s_PROJ : constant option list }
-val declare_structure :
- inductive * constructor * (name * bool) list * constant option list -> unit
+type struc_tuple =
+ inductive * constructor * (name * bool) list * constant option list
+
+val declare_structure : struc_tuple -> unit
-(* [lookup_structure isp] returns the struc_typ associated to the
+(** [lookup_structure isp] returns the struc_typ associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val lookup_structure : inductive -> struc_typ
-(* [lookup_projections isp] returns the projections associated to the
+(** [lookup_projections isp] returns the projections associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val lookup_projections : inductive -> constant option list
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
val find_projection_nparams : global_reference -> int
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
val find_projection : global_reference -> struc_typ
-(* we keep an index (dnet) of record's arguments + fields
+(** we keep an index (dnet) of record's arguments + fields
(=methods). Here is how to declare them: *)
val declare_method :
global_reference -> Evd.evar -> Evd.evar_map -> unit
- (* and here is how to search for methods matched by a given term: *)
+ (** and here is how to search for methods matched by a given term: *)
val methods_matching : constr ->
((global_reference*Evd.evar*Evd.evar_map) *
(constr*existential_key)*Termops.subst) list
-(*s A canonical structure declares "canonical" conversion hints between *)
-(* the effective components of a structure and the projections of the *)
-(* structure *)
+(** {6 Canonical structures } *)
+(** A canonical structure declares "canonical" conversion hints between
+ the effective components of a structure and the projections of the
+ structure *)
type cs_pattern =
Const_cs of global_reference
@@ -66,11 +68,11 @@ type cs_pattern =
type obj_typ = {
o_DEF : constr;
- o_INJ : int; (* position of trivial argument *)
- o_TABS : constr list; (* ordered *)
- o_TPARAMS : constr list; (* ordered *)
+ o_INJ : int; (** position of trivial argument *)
+ o_TABS : constr list; (** ordered *)
+ o_TPARAMS : constr list; (** ordered *)
o_NPARAMS : int;
- o_TCOMPS : constr list } (* ordered *)
+ o_TCOMPS : constr list } (** ordered *)
val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
@@ -78,6 +80,6 @@ val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
val declare_canonical_structure : global_reference -> unit
val is_open_canonical_projection :
- Evd.evar_map -> (constr * constr list) -> bool
+ Environ.env -> Evd.evar_map -> (constr * constr list) -> bool
val canonical_projections : unit ->
((global_reference * cs_pattern) * obj_typ) list