diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 32 |
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 |