diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cClosure.ml | 2 | ||||
-rw-r--r-- | kernel/cClosure.mli | 6 | ||||
-rw-r--r-- | kernel/constr.mli | 22 | ||||
-rw-r--r-- | kernel/environ.mli | 2 | ||||
-rw-r--r-- | kernel/evar.ml | 1 | ||||
-rw-r--r-- | kernel/evar.mli | 3 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/term.mli | 20 | ||||
-rw-r--r-- | kernel/typeops.mli | 2 |
10 files changed, 34 insertions, 28 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fa12e5406..31ded9129 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -234,7 +234,7 @@ let unfold_red kn = * instantiations (cbv or lazy) are. *) -type table_key = Constant.t puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey let eq_pconstant_key (c,u) (c',u') = eq_constant_key c c' && Univ.Instance.equal u u' diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 28136e1fc..119b70e30 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -92,7 +92,7 @@ val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds (***********************************************************************) -type table_key = Constant.t puniverses tableKey +type table_key = Constant.t Univ.puniverses tableKey type 'a infos_cache type 'a infos = { @@ -122,8 +122,8 @@ type fterm = | FAtom of constr (** Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive puniverses - | FConstruct of constructor puniverses + | FInd of inductive Univ.puniverses + | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array | FProj of projection * fconstr | FFix of fixpoint * fconstr subs diff --git a/kernel/constr.mli b/kernel/constr.mli index 4c5ea9e95..21c477578 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -13,20 +13,22 @@ open Names (** {6 Value under universe substitution } *) type 'a puniverses = 'a Univ.puniverses +[@@ocaml.deprecated "use Univ.puniverses"] (** {6 Simply type aliases } *) -type pconstant = Constant.t puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses +type pconstant = Constant.t Univ.puniverses +type pinductive = inductive Univ.puniverses +type pconstructor = constructor Univ.puniverses (** {6 Existential variables } *) type existential_key = Evar.t +[@@ocaml.deprecated "use Evar.t"] (** {6 Existential variables } *) type metavariable = int (** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) @@ -80,7 +82,7 @@ val mkVar : Id.t -> constr val mkMeta : metavariable -> constr (** Constructs an existential variable *) -type existential = existential_key * constr array +type existential = Evar.t * constr array val mkEvar : existential -> constr (** Construct a sort *) @@ -111,7 +113,7 @@ val mkLetIn : Name.t * constr * types * constr -> constr {%latex:$(f~t_1\dots f_n)$%}. *) val mkApp : constr * constr array -> constr -val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses +val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses (** Constructs a Constant.t *) val mkConst : Constant.t -> constr @@ -180,7 +182,7 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) -type 'constr pexistential = existential_key * 'constr array +type 'constr pexistential = Evar.t * 'constr array type ('constr, 'types) prec_declaration = Name.t array * 'types array * 'constr array type ('constr, 'types) pfixpoint = @@ -295,16 +297,16 @@ val decompose_app : constr -> constr * constr list val decompose_appvect : constr -> constr * constr array (** Destructs a constant *) -val destConst : constr -> Constant.t puniverses +val destConst : constr -> Constant.t Univ.puniverses (** Destructs an existential variable *) val destEvar : constr -> existential (** Destructs a (co)inductive type *) -val destInd : constr -> inductive puniverses +val destInd : constr -> inductive Univ.puniverses (** Destructs a constructor *) -val destConstruct : constr -> constructor puniverses +val destConstruct : constr -> constructor Univ.puniverses (** Destructs a [match c as x in I args return P with ... | Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args diff --git a/kernel/environ.mli b/kernel/environ.mli index f2066b065..652ed0f9f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -7,8 +7,8 @@ (************************************************************************) open Names -open Univ open Constr +open Univ open Declarations (** Unsafe environments. We define here a datatype for environments. diff --git a/kernel/evar.ml b/kernel/evar.ml index e63665f51..dcd2e12a0 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -13,6 +13,7 @@ let unsafe_of_int x = x let compare = Int.compare let equal = Int.equal let hash = Int.hash +let print x = Pp.(str "?X" ++ int x) module Set = Int.Set module Map = Int.Map diff --git a/kernel/evar.mli b/kernel/evar.mli index eee6680fb..6a058207f 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -30,5 +30,8 @@ val compare : t -> t -> int val hash : t -> int (** Hash over existential variables. *) +val print : t -> Pp.t +(** Printing representation *) + module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 601422a10..a19f87b05 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -7,8 +7,8 @@ (************************************************************************) open Names -open Univ open Constr +open Univ open Declarations open Environ diff --git a/kernel/term.ml b/kernel/term.ml index 4217cfac7..aa8805952 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -31,7 +31,7 @@ type constr = Constr.t type types = Constr.t (** Same as [constr], for documentation purposes. *) -type existential_key = Constr.existential_key +type existential_key = Evar.t type existential = Constr.existential type metavariable = Constr.metavariable diff --git a/kernel/term.mli b/kernel/term.mli index 4efb582d0..f5cb72f4e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -129,7 +129,7 @@ val decompose_appvect : constr -> constr * constr array [@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] (** Destructs a constant *) -val destConst : constr -> Constant.t puniverses +val destConst : constr -> Constant.t Univ.puniverses [@@ocaml.deprecated "Alias for [Constr.destConst]"] (** Destructs an existential variable *) @@ -137,11 +137,11 @@ val destEvar : constr -> existential [@@ocaml.deprecated "Alias for [Constr.destEvar]"] (** Destructs a (co)inductive type *) -val destInd : constr -> inductive puniverses +val destInd : constr -> inductive Univ.puniverses [@@ocaml.deprecated "Alias for [Constr.destInd]"] (** Destructs a constructor *) -val destConstruct : constr -> constructor puniverses +val destConstruct : constr -> constructor Univ.puniverses [@@ocaml.deprecated "Alias for [Constr.destConstruct]"] (** Destructs a [match c as x in I args return P with ... | @@ -407,11 +407,11 @@ val mkInd : inductive -> constr [@@ocaml.deprecated "Alias for Constr"] val mkConstruct : constructor -> constr [@@ocaml.deprecated "Alias for Constr"] -val mkConstU : Constant.t puniverses -> constr +val mkConstU : Constant.t Univ.puniverses -> constr [@@ocaml.deprecated "Alias for Constr"] -val mkIndU : inductive puniverses -> constr +val mkIndU : inductive Univ.puniverses -> constr [@@ocaml.deprecated "Alias for Constr"] -val mkConstructU : constructor puniverses -> constr +val mkConstructU : constructor Univ.puniverses -> constr [@@ocaml.deprecated "Alias for Constr"] val mkConstructUi : (pinductive * int) -> constr [@@ocaml.deprecated "Alias for Constr"] @@ -461,7 +461,7 @@ val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr [@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] -val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses +val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses [@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] val univ_of_sort : Sorts.t -> Univ.Universe.t [@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] @@ -497,7 +497,7 @@ type sorts = Sorts.t = type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] -type 'a puniverses = 'a Constr.puniverses +type 'a puniverses = 'a Univ.puniverses [@@ocaml.deprecated "Alias for Constr.puniverses"] (** Simply type aliases *) @@ -507,8 +507,8 @@ type pinductive = Constr.pinductive [@@ocaml.deprecated "Alias for Constr.pinductive"] type pconstructor = Constr.pconstructor [@@ocaml.deprecated "Alias for Constr.pconstructor"] -type existential_key = Constr.existential_key -[@@ocaml.deprecated "Alias for Constr.existential_key"] +type existential_key = Evar.t +[@@ocaml.deprecated "Alias for Evar.t"] type existential = Constr.existential [@@ocaml.deprecated "Alias for Constr.existential"] type metavariable = Constr.metavariable diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3aaad5877..5584b6ab4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -7,8 +7,8 @@ (************************************************************************) open Names -open Univ open Constr +open Univ open Environ open Entries |