diff options
Diffstat (limited to 'pretyping/recordops.mli')
| -rw-r--r-- | pretyping/recordops.mli | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index a6a90c75..1f7b23c0 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,13 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names -open Term +open Constr open Globnames (** Operations concerning records and canonical structures *) @@ -20,10 +22,10 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list val declare_structure : struc_tuple -> unit @@ -35,7 +37,7 @@ val lookup_structure : inductive -> struc_typ (** [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 +val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int @@ -52,12 +54,12 @@ val find_projection : global_reference -> struc_typ type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) @@ -65,13 +67,13 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list -val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds +val pr_cs_pattern : cs_pattern -> Pp.t 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 Reductionops.Stack.t) -> bool + Environ.env -> Evd.evar_map -> Reductionops.state -> bool val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list |