summaryrefslogtreecommitdiff
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /pretyping/recordops.mli
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'pretyping/recordops.mli')
-rw-r--r--pretyping/recordops.mli32
1 files changed, 12 insertions, 20 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 442e51db..37d5b4c2 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,17 +1,14 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Names
-open Nametab
open Term
-open Libnames
-open Libobject
-open Library
+open Globnames
(** Operations concerning records and canonical structures *)
@@ -22,11 +19,11 @@ open Library
type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
- s_PROJKIND : (name * bool) list;
+ s_PROJKIND : (Name.t * bool) list;
s_PROJ : constant option list }
type struc_tuple =
- inductive * constructor * (name * bool) list * constant option list
+ inductive * constructor * (Name.t * bool) list * constant option list
val declare_structure : struc_tuple -> unit
@@ -46,20 +43,12 @@ val find_projection_nparams : global_reference -> int
(** raise [Not_found] if not a projection *)
val find_projection : global_reference -> struc_typ
-(** 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: *)
-val methods_matching : constr ->
- ((global_reference*Evd.evar*Evd.evar_map) *
- (constr*existential_key)*Termops.subst) list
-
(** {6 Canonical structures } *)
(** A canonical structure declares "canonical" conversion hints between
the effective components of a structure and the projections of the
structure *)
+(** A cs_pattern characterizes the form of a component of canonical structure *)
type cs_pattern =
Const_cs of global_reference
| Prod_cs
@@ -68,18 +57,21 @@ type cs_pattern =
type obj_typ = {
o_DEF : constr;
- o_INJ : int; (** position of trivial argument *)
+ o_CTX : Univ.ContextSet.t;
+ o_INJ : int option; (** position of trivial argument *)
o_TABS : constr list; (** ordered *)
o_TPARAMS : constr list; (** ordered *)
o_NPARAMS : int;
o_TCOMPS : constr list } (** ordered *)
-val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
+(** Return the form of the component of a canonical structure *)
+val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+
val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
val declare_canonical_structure : global_reference -> unit
val is_open_canonical_projection :
- Environ.env -> Evd.evar_map -> (constr * constr list) -> bool
+ Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
val canonical_projections : unit ->
((global_reference * cs_pattern) * obj_typ) list