diff options
64 files changed, 16 insertions, 1117 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml index b9dcfd61d1..d3fa4ef65e 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -49,10 +49,6 @@ sig val map_to_list : ('a -> 'b) -> 'a array -> 'b list val map_of_list : ('a -> 'b) -> 'a list -> 'b array val chop : int -> 'a array -> 'a array * 'a array - val smartmap : ('a -> 'a) -> 'a array -> 'a array - [@@ocaml.deprecated "Same as [Smart.map]"] - val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array - [@@ocaml.deprecated "Same as [Smart.fold_left_map]"] val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array val map3 : @@ -65,13 +61,6 @@ sig val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array val fold_left2_map_i : (int -> 'a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array - [@@ocaml.deprecated "Same as [fold_left_map]"] - val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c - [@@ocaml.deprecated "Same as [fold_right_map]"] - val fold_map2' : - ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - [@@ocaml.deprecated "Same as [fold_right2_map]"] val distinct : 'a array -> bool val rev_of_list : 'a list -> 'a array val rev_to_list : 'a array -> 'a list @@ -86,8 +75,6 @@ sig module Fun1 : sig val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array - val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array - [@@ocaml.deprecated "Same as [Fun1.Smart.map]"] val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit module Smart : @@ -429,15 +416,11 @@ else let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in (v',!e') -let fold_map' = fold_right_map - let fold_left_map f e v = let e' = ref e in let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in (!e',v') -let fold_map = fold_left_map - let fold_right2_map f v1 v2 e = let e' = ref e in let v' = @@ -445,8 +428,6 @@ let fold_right2_map f v1 v2 e = in (v',!e') -let fold_map2' = fold_right2_map - let fold_left2_map f e v1 v2 = let e' = ref e in let v' = map2 (fun x1 x2 -> let (e,y) = f !e' x1 x2 in e' := e; y) v1 v2 in @@ -617,10 +598,6 @@ struct end -(* Deprecated aliases *) -let smartmap = Smart.map -let smartfoldmap = Smart.fold_left_map - module Fun1 = struct @@ -687,6 +664,4 @@ struct end - let smartmap = Smart.map - end diff --git a/clib/cArray.mli b/clib/cArray.mli index 163191681a..f5b015b206 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -82,12 +82,6 @@ sig (** [chop i a] returns [(a1, a2)] s.t. [a = a1 + a2] and [length a1 = n]. Raise [Failure "Array.chop"] if [i] is not a valid index. *) - val smartmap : ('a -> 'a) -> 'a array -> 'a array - [@@ocaml.deprecated "Same as [Smart.map]"] - - val smartfoldmap : ('r -> 'a -> 'r * 'a) -> 'r -> 'a array -> 'r * 'a array - [@@ocaml.deprecated "Same as [Smart.fold_left_map]"] - val map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array (** See also [Smart.map2] *) @@ -121,16 +115,6 @@ sig val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c (** Same with two arrays, folding on the left *) - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array - [@@ocaml.deprecated "Same as [fold_left_map]"] - - val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c - [@@ocaml.deprecated "Same as [fold_right_map]"] - - val fold_map2' : - ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - [@@ocaml.deprecated "Same as [fold_right2_map]"] - val distinct : 'a array -> bool (** Return [true] if every element of the array is unique (for default equality). *) @@ -175,9 +159,6 @@ sig val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array (** [Fun1.map f x v = map (f x) v] *) - val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array - [@@ocaml.deprecated "Same as [Fun1.Smart.map]"] - val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit (** [Fun1.iter f x v = iter (f x) v] *) diff --git a/clib/cList.ml b/clib/cList.ml index dc59ff2970..aba3e46bd5 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -36,16 +36,12 @@ sig val filteri : (int -> 'a -> bool) -> 'a list -> 'a list val filter_with : bool list -> 'a list -> 'a list - val smartfilter : ('a -> bool) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [filter]"] val map_filter : ('a -> 'b option) -> 'a list -> 'b list val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list val map : ('a -> 'b) -> 'a list -> 'b list val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - val smartmap : ('a -> 'a) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list val map2_i : @@ -75,10 +71,6 @@ sig val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - [@@ocaml.deprecated "Same as [fold_left_map]"] - val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - [@@ocaml.deprecated "Same as [fold_right_map]"] val except : 'a eq -> 'a -> 'a list -> 'a list val remove : 'a eq -> 'a -> 'a list -> 'a list val remove_first : ('a -> bool) -> 'a list -> 'a list @@ -116,8 +108,6 @@ sig val unionq : 'a list -> 'a list -> 'a list val subtract : 'a eq -> 'a list -> 'a list -> 'a list val subtractq : 'a list -> 'a list -> 'a list - val merge_uniq : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [merge_set]"] val distinct : 'a list -> bool val distinct_f : 'a cmp -> 'a list -> bool val duplicates : 'a eq -> 'a list -> 'a list @@ -337,8 +327,6 @@ let filteri p = in filter_i_rec 0 -let smartfilter = filter (* Alias *) - let rec filter_with_loop filter p l = match filter, l with | [], [] -> () | b :: filter, x :: l' -> @@ -618,8 +606,6 @@ let rec fold_left_map f e = function let e'',t' = fold_left_map f e' t in e'',h' :: t' -let fold_map = fold_left_map - (* (* tail-recursive version of the above function *) let fold_left_map f e l = let g (e,b') h = @@ -634,8 +620,6 @@ let fold_left_map f e l = let fold_right_map f l e = List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e) -let fold_map' = fold_right_map - let on_snd f (x,y) = (x,f y) let fold_left2_map f e l l' = @@ -905,8 +889,6 @@ let rec merge_set cmp l1 l2 = match l1, l2 with then h1 :: merge_set cmp t1 l2 else h2 :: merge_set cmp l1 t2 -let merge_uniq = merge_set - let intersect cmp l1 l2 = filter (fun x -> mem_f cmp x l2) l1 @@ -1047,8 +1029,6 @@ struct end -let smartmap = Smart.map - module type MonoS = sig type elt val equal : elt list -> elt list -> bool diff --git a/clib/cList.mli b/clib/cList.mli index 39d9a5e535..8582e6cd65 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -91,9 +91,6 @@ sig (** [filter_with bl l] selects elements of [l] whose corresponding element in [bl] is [true]. Raise [Invalid_argument _] if sizes differ. *) - val smartfilter : ('a -> bool) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [filter]"] - val map_filter : ('a -> 'b option) -> 'a list -> 'b list (** Like [map] but keeping only non-[None] elements *) @@ -111,9 +108,6 @@ sig val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list (** Like OCaml [List.map2] but tail-recursive *) - val smartmap : ('a -> 'a) -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [Smart.map]"] - val map_left : ('a -> 'b) -> 'a list -> 'b list (** As [map] but ensures the left-to-right order of evaluation. *) @@ -208,12 +202,6 @@ sig val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list (** Same with four lists, folding on the left *) - val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - [@@ocaml.deprecated "Same as [fold_left_map]"] - - val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - [@@ocaml.deprecated "Same as [fold_right_map]"] - (** {6 Splitting} *) val except : 'a eq -> 'a -> 'a list -> 'a list @@ -357,9 +345,6 @@ sig val subtractq : 'a list -> 'a list -> 'a list (** [subtract] specialized to physical equality *) - val merge_uniq : 'a cmp -> 'a list -> 'a list -> 'a list - [@@ocaml.deprecated "Same as [merge_set]"] - (** {6 Uniqueness and duplication} *) val distinct : 'a list -> bool diff --git a/clib/cMap.ml b/clib/cMap.ml index 54a8b25851..040dede0a2 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -34,10 +34,6 @@ sig val bind : (key -> 'a) -> Set.t -> 'a t val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b - val smartmap : ('a -> 'a) -> 'a t -> 'a t - [@@ocaml.deprecated "Same as [Smart.map]"] - val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a t -> int module Smart : sig @@ -65,10 +61,6 @@ sig val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b - val smartmap : ('a -> 'a) -> 'a map -> 'a map - [@@ocaml.deprecated "Same as [Smart.map]"] - val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map - [@@ocaml.deprecated "Same as [Smart.mapi]"] val height : 'a map -> int module Smart : sig @@ -195,9 +187,6 @@ struct end - let smartmap = Smart.map - let smartmapi = Smart.mapi - module Unsafe = struct diff --git a/clib/cMap.mli b/clib/cMap.mli index 127bf23ab6..f5496239f6 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -57,12 +57,6 @@ sig val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b (** Folding keys in decreasing order. *) - val smartmap : ('a -> 'a) -> 'a t -> 'a t - [@@ocaml.deprecated "Same as [Smart.map]"] - - val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t - [@@ocaml.deprecated "Same as [Smart.mapi]"] - val height : 'a t -> int (** An indication of the logarithmic size of a map *) diff --git a/clib/hMap.ml b/clib/hMap.ml index b2cf474304..33cb6d0131 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -396,9 +396,6 @@ struct end - let smartmap = Smart.map - let smartmapi = Smart.mapi - let height s = Int.Map.height s module Unsafe = diff --git a/clib/option.ml b/clib/option.ml index 7a3d5f934f..3e57fd5c85 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -131,8 +131,6 @@ let fold_right_map f x a = | Some y -> let z, a = f y a in Some z, a | _ -> None, a -let fold_map = fold_left_map - (** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) let cata f a = function | Some c -> f c @@ -183,8 +181,6 @@ struct end -let smartmap = Smart.map - (** {6 Operations with Lists} *) module List = diff --git a/clib/option.mli b/clib/option.mli index 8f82bf090b..e99c8015c4 100644 --- a/clib/option.mli +++ b/clib/option.mli @@ -75,9 +75,6 @@ val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit (** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) val map : ('a -> 'b) -> 'a option -> 'b option -val smartmap : ('a -> 'a) -> 'a option -> 'a option -[@@ocaml.deprecated "Same as [Smart.map]"] - (** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b @@ -95,10 +92,6 @@ val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option (** Same as [fold_left_map] on the right *) val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a -(** @deprecated Same as [fold_left_map] *) -val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option -[@@ocaml.deprecated "Same as [fold_left_map]"] - (** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b diff --git a/dev/base_include b/dev/base_include index 6f54ecb241..67a7e87d78 100644 --- a/dev/base_include +++ b/dev/base_include @@ -99,7 +99,6 @@ open Evarutil open Evarsolve open Tacred open Evd -open Universes open Termops open Namegen open Indrec diff --git a/dev/doc/changes.md b/dev/doc/changes.md index d6d296f012..7e64f80ac5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +General deprecation + +- All functions marked [@@ocaml.deprecated] in 8.8 have been + removed. Please, make sure your plugin is warning-free in 8.8 before + trying to port it over 8.9. + Names - Kernel names no longer contain a section path. They now have only two diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b1d880b0ad..fc2189f870 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -11,7 +11,6 @@ open CErrors open Util open Names -open Term open Constr open Environ open Evd @@ -43,9 +42,6 @@ let evd_comb2 f evdref x y = evdref := evd'; z -let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x - let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in (evd, c) @@ -87,23 +83,6 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = let nf_evars_universes evm = UnivSubst.nf_evars_and_universes_opt_subst (safe_evar_value evm) (Evd.universe_subst evm) - -let nf_evars_and_universes evm = - let evm = Evd.minimize_universes evm in - evm, nf_evars_universes evm - -let e_nf_evars_and_universes evdref = - evdref := Evd.minimize_universes !evdref; - nf_evars_universes !evdref, Evd.universe_subst !evdref - -let nf_evar_map_universes evm = - let evm = Evd.minimize_universes evm in - let subst = Evd.universe_subst evm in - if Univ.LMap.is_empty subst then evm, nf_evar0 evm - else - let f = nf_evars_universes evm in - let f' c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in - Evd.raw_map (fun _ -> map_evar_info f') evm, f let nf_named_context_evar sigma ctx = Context.Named.map (nf_evar0 sigma) ctx @@ -490,26 +469,11 @@ let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in - evdref := evd; - c - let new_Type ?(rigid=Evd.univ_flexible) evd = let open EConstr in let (evd, s) = new_sort_variable rigid evd in (evd, mkSort s) -let e_new_Type ?(rigid=Evd.univ_flexible) evdref = - let evd', s = new_sort_variable rigid !evdref in - evdref := evd'; EConstr.mkSort s - - (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in - evdref := evd'; - ev - (* Safe interface to unification problems *) type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr @@ -853,7 +817,7 @@ let occur_evar_upto sigma n c = let judge_of_new_Type evd = let open EConstr in let (evd', s) = new_univ_variable univ_rigid evd in - (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }) + (evd', { uj_val = mkSort (Sorts.Type s); uj_type = mkSort (Sorts.Type (Univ.super s)) }) let subterm_source evk ?where (loc,k) = let evk = match k with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 0ad323ac4b..1046fdc8d8 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -173,14 +173,6 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr -val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] - -(** Normalize the evar map w.r.t. universes, after simplification of constraints. - Return the substitution function for constrs as well. *) -val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] - (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t val flush_and_check_evars : evar_map -> constr -> Constr.constr @@ -273,25 +265,3 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo Evar_kinds.t Loc.located val meta_counter_summary_tag : int Summary.Dyn.tag - -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> constr -[@@ocaml.deprecated "Use [Evarutil.new_evar]"] - -val e_new_type_evar : env -> evar_map ref -> - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t -[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] - -val e_new_Type : ?rigid:rigid -> evar_map ref -> constr -[@@ocaml.deprecated "Use [Evarutil.new_Type]"] - -val e_new_global : evar_map ref -> GlobRef.t -> constr -[@@ocaml.deprecated "Use [Evarutil.new_global]"] - -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst -[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] diff --git a/engine/termops.mli b/engine/termops.mli index 0e5d564d3f..64e3977d68 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -335,16 +335,4 @@ val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t -val print_constr : constr -> Pp.t -[@@deprecated "use print_constr_env"] - end - -val print_constr : constr -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] - -val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, it is *extremely* likely that you want to use [Printer.pr_econstr_env] instead"] - -val print_rel_context : env -> Pp.t -[@@deprecated "This is an internal, debug printer. WARNING, this function is not suitable for plugin code, if you still want to use it then call [Internal.print_rel_context] instead"] diff --git a/engine/universes.ml b/engine/universes.ml deleted file mode 100644 index 5d0157b2db..0000000000 --- a/engine/universes.ml +++ /dev/null @@ -1,92 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Univ - -(** Deprecated *) - -(** UnivNames *) -type universe_binders = UnivNames.universe_binders -type univ_name_list = UnivNames.univ_name_list - -let pr_with_global_universes = UnivNames.pr_with_global_universes -let reference_of_level = UnivNames.qualid_of_level - -let empty_binders = UnivNames.empty_binders - -let register_universe_binders = UnivNames.register_universe_binders - -let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names - -(** UnivGen *) -type universe_id = UnivGen.universe_id - -let set_remote_new_univ_id = UnivGen.set_remote_new_univ_id -let new_univ_id = UnivGen.new_univ_id -let new_univ_level = UnivGen.new_univ_level -let new_univ = UnivGen.new_univ -let new_Type = UnivGen.new_Type -let new_Type_sort = UnivGen.new_Type_sort -let new_global_univ = UnivGen.new_global_univ -let new_sort_in_family = UnivGen.new_sort_in_family -let fresh_instance_from_context = UnivGen.fresh_instance_from_context -let fresh_instance_from = UnivGen.fresh_instance_from -let fresh_sort_in_family = UnivGen.fresh_sort_in_family -let fresh_constant_instance = UnivGen.fresh_constant_instance -let fresh_inductive_instance = UnivGen.fresh_inductive_instance -let fresh_constructor_instance = UnivGen.fresh_constructor_instance -let fresh_global_instance = UnivGen.fresh_global_instance -let fresh_global_or_constr_instance = UnivGen.fresh_global_or_constr_instance -let fresh_universe_context_set_instance = UnivGen.fresh_universe_context_set_instance -let global_of_constr = UnivGen.global_of_constr -let constr_of_global_univ = UnivGen.constr_of_global_univ -let extend_context = UnivGen.extend_context -let constr_of_global = UnivGen.constr_of_global -let constr_of_reference = UnivGen.constr_of_global -let type_of_global = UnivGen.type_of_global - -(** UnivSubst *) - -let level_subst_of = UnivSubst.level_subst_of -let subst_univs_constraints = UnivSubst.subst_univs_constraints -let subst_univs_constr = UnivSubst.subst_univs_constr -type universe_opt_subst = UnivSubst.universe_opt_subst -let make_opt_subst = UnivSubst.make_opt_subst -let subst_opt_univs_constr = UnivSubst.subst_opt_univs_constr -let normalize_univ_variables = UnivSubst.normalize_univ_variables -let normalize_univ_variable = UnivSubst.normalize_univ_variable -let normalize_univ_variable_opt_subst = UnivSubst.normalize_univ_variable_opt_subst -let normalize_univ_variable_subst = UnivSubst.normalize_univ_variable_subst -let normalize_universe_opt_subst = UnivSubst.normalize_universe_opt_subst -let normalize_universe_subst = UnivSubst.normalize_universe_subst -let nf_evars_and_universes_opt_subst = UnivSubst.nf_evars_and_universes_opt_subst -let pr_universe_opt_subst = UnivSubst.pr_universe_opt_subst - -(** UnivProblem *) - -type universe_constraint = UnivProblem.t = - | ULe of Universe.t * Universe.t - | UEq of Universe.t * Universe.t - | ULub of Level.t * Level.t - | UWeak of Level.t * Level.t - -module Constraints = UnivProblem.Set -type 'a constraint_accumulator = 'a UnivProblem.accumulator -type 'a universe_constrained = 'a UnivProblem.constrained -type 'a universe_constraint_function = 'a UnivProblem.constraint_function -let subst_univs_universe_constraints = UnivProblem.Set.subst_univs -let enforce_eq_instances_univs = UnivProblem.enforce_eq_instances_univs -let to_constraints = UnivProblem.to_constraints -let eq_constr_univs_infer_with = UnivProblem.eq_constr_univs_infer_with - -(** UnivMinim *) -module UPairSet = UnivMinim.UPairSet - -let normalize_context_set = UnivMinim.normalize_context_set diff --git a/engine/universes.mli b/engine/universes.mli deleted file mode 100644 index 0d3bae4c95..0000000000 --- a/engine/universes.mli +++ /dev/null @@ -1,230 +0,0 @@ -(************************************************************************) -(* * 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 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names -open Constr -open Environ -open Univ - -(** ************************************** *) -(** This entire module is deprecated. **** *) -(** ************************************** *) -[@@@ocaml.warning "-3"] - -(** ****** Deprecated: moved to [UnivNames] *) - -val pr_with_global_universes : Level.t -> Pp.t -[@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"] -val reference_of_level : Level.t -> Libnames.qualid -[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] - -type universe_binders = UnivNames.universe_binders -[@@ocaml.deprecated "Use [UnivNames.universe_binders]"] - -val empty_binders : universe_binders -[@@ocaml.deprecated "Use [UnivNames.empty_binders]"] - -val register_universe_binders : Globnames.global_reference -> universe_binders -> unit -[@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"] - -type univ_name_list = UnivNames.univ_name_list -[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] - -val universe_binders_with_opt_names : Globnames.global_reference -> - univ_name_list option -> universe_binders -[@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] - -(** ****** Deprecated: moved to [UnivGen] *) - -type universe_id = UnivGen.universe_id -[@@ocaml.deprecated "Use [UnivGen.universe_id]"] - -val set_remote_new_univ_id : universe_id RemoteCounter.installer -[@@ocaml.deprecated "Use [UnivGen.set_remote_new_univ_id]"] - -val new_univ_id : unit -> universe_id -[@@ocaml.deprecated "Use [UnivGen.new_univ_id]"] - -val new_univ_level : unit -> Level.t -[@@ocaml.deprecated "Use [UnivGen.new_univ_level]"] - -val new_univ : unit -> Universe.t -[@@ocaml.deprecated "Use [UnivGen.new_univ]"] - -val new_Type : unit -> types -[@@ocaml.deprecated "Use [UnivGen.new_Type]"] - -val new_Type_sort : unit -> Sorts.t -[@@ocaml.deprecated "Use [UnivGen.new_Type_sort]"] - -val new_global_univ : unit -> Universe.t in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.new_global_univ]"] - -val new_sort_in_family : Sorts.family -> Sorts.t -[@@ocaml.deprecated "Use [UnivGen.new_sort_in_family]"] - -val fresh_instance_from_context : AUContext.t -> - Instance.t constrained -[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from_context]"] - -val fresh_instance_from : AUContext.t -> Instance.t option -> - Instance.t in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] - -val fresh_sort_in_family : Sorts.family -> - Sorts.t in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] - -val fresh_constant_instance : env -> Constant.t -> - pconstant in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_constant_instance]"] - -val fresh_inductive_instance : env -> inductive -> - pinductive in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_inductive_instance]"] - -val fresh_constructor_instance : env -> constructor -> - pconstructor in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_constructor_instance]"] - -val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> - constr in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_global_instance]"] - -val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> - constr in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.fresh_global_or_constr_instance]"] - -val fresh_universe_context_set_instance : ContextSet.t -> - universe_level_subst * ContextSet.t -[@@ocaml.deprecated "Use [UnivGen.fresh_universe_context_set_instance]"] - -val global_of_constr : constr -> Globnames.global_reference puniverses -[@@ocaml.deprecated "Use [UnivGen.global_of_constr]"] - -val constr_of_global_univ : Globnames.global_reference puniverses -> constr -[@@ocaml.deprecated "Use [UnivGen.constr_of_global_univ]"] - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.extend_context]"] - -val constr_of_global : Globnames.global_reference -> constr -[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] - -val constr_of_reference : Globnames.global_reference -> constr -[@@ocaml.deprecated "Use [UnivGen.constr_of_global]"] - -val type_of_global : Globnames.global_reference -> types in_universe_context_set -[@@ocaml.deprecated "Use [UnivGen.type_of_global]"] - -(** ****** Deprecated: moved to [UnivSubst] *) - -val level_subst_of : universe_subst_fn -> universe_level_subst_fn -[@@ocaml.deprecated "Use [UnivSubst.level_subst_of]"] - -val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t -[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constraints]"] - -val subst_univs_constr : universe_subst -> constr -> constr -[@@ocaml.deprecated "Use [UnivSubst.subst_univs_constr]"] - -type universe_opt_subst = UnivSubst.universe_opt_subst -[@@ocaml.deprecated "Use [UnivSubst.universe_opt_subst]"] - -val make_opt_subst : universe_opt_subst -> universe_subst_fn -[@@ocaml.deprecated "Use [UnivSubst.make_opt_subst]"] - -val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -[@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"] - -val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * universe_subst -[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"] - -val normalize_univ_variable : - find:(Level.t -> Universe.t) -> - Level.t -> Universe.t -[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable]"] - -val normalize_univ_variable_opt_subst : universe_opt_subst -> - (Level.t -> Universe.t) -[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_opt_subst]"] - -val normalize_univ_variable_subst : universe_subst -> - (Level.t -> Universe.t) -[@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variable_subst]"] - -val normalize_universe_opt_subst : universe_opt_subst -> - (Universe.t -> Universe.t) -[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_opt_subst]"] - -val normalize_universe_subst : universe_subst -> - (Universe.t -> Universe.t) -[@@ocaml.deprecated "Use [UnivSubst.normalize_universe_subst]"] - -val nf_evars_and_universes_opt_subst : (existential -> constr option) -> - universe_opt_subst -> constr -> constr -[@@ocaml.deprecated "Use [UnivSubst.nf_evars_and_universes_opt_subst]"] - -val pr_universe_opt_subst : universe_opt_subst -> Pp.t -[@@ocaml.deprecated "Use [UnivSubst.pr_universe_opt_subst]"] - -(** ****** Deprecated: moved to [UnivProblem] *) - -type universe_constraint = UnivProblem.t = - | ULe of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.ULe]"] - | UEq of Universe.t * Universe.t [@ocaml.deprecated "Use [UnivProblem.UEq]"] - | ULub of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.ULub]"] - | UWeak of Level.t * Level.t [@ocaml.deprecated "Use [UnivProblem.UWeak]"] -[@@ocaml.deprecated "Use [UnivProblem.t]"] - -module Constraints = UnivProblem.Set -[@@ocaml.deprecated "Use [UnivProblem.Set]"] - -type 'a constraint_accumulator = 'a UnivProblem.accumulator -[@@ocaml.deprecated "Use [UnivProblem.accumulator]"] -type 'a universe_constrained = 'a UnivProblem.constrained -[@@ocaml.deprecated "Use [UnivProblem.constrained]"] -type 'a universe_constraint_function = 'a UnivProblem.constraint_function -[@@ocaml.deprecated "Use [UnivProblem.constraint_function]"] - -val subst_univs_universe_constraints : universe_subst_fn -> - Constraints.t -> Constraints.t -[@@ocaml.deprecated "Use [UnivProblem.Set.subst_univs]"] - -val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -[@@ocaml.deprecated "Use [UnivProblem.enforce_eq_instances_univs]"] - -(** With [force_weak] UWeak constraints are turned into equalities, - otherwise they're forgotten. *) -val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Constraint.t -[@@ocaml.deprecated "Use [UnivProblem.to_constraints]"] - -(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of - {!eq_constr_univs_infer} taking kind-of-term functions, to expose - subterms of [m] and [n], arguments. *) -val eq_constr_univs_infer_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -[@@ocaml.deprecated "Use [UnivProblem.eq_constr_univs_infer_with]"] - -(** ****** Deprecated: moved to [UnivMinim] *) - -module UPairSet = UnivMinim.UPairSet -[@@ocaml.deprecated "Use [UnivMinim.UPairSet]"] - -val normalize_context_set : UGraph.t -> ContextSet.t -> - universe_opt_subst (* The defined and undefined variables *) -> - LSet.t (* univ variables that can be substituted by algebraics *) -> - UPairSet.t (* weak equality constraints *) -> - (universe_opt_subst * LSet.t) in_universe_context_set -[@@ocaml.deprecated "Use [UnivMinim.normalize_context_set]"] diff --git a/kernel/constr.mli b/kernel/constr.mli index 2efdae007c..3c9cc96a0d 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -13,20 +13,12 @@ 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 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 } *) diff --git a/kernel/environ.mli b/kernel/environ.mli index 1343b9029b..55ff7ff162 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -320,8 +320,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat open Retroknowledge (** functions manipulating the retroknowledge @author spiwack *) -val retroknowledge : (retroknowledge->'a) -> env -> 'a -[@@ocaml.deprecated "Use the record projection."] val registered : env -> field -> bool diff --git a/kernel/names.ml b/kernel/names.ml index 1e28ec51fb..7cd749de1d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -739,15 +739,12 @@ let eq_table_key f ik1 ik2 = | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_con_chk = Constant.UserOrd.equal let eq_mind_chk = MutInd.UserOrd.equal let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 - (*******************************************************************) (** Compatibility layers *) -type mod_bound_id = MBId.t let eq_constant_key = Constant.UserOrd.equal (** Compatibility layer for [ModPath] *) @@ -923,8 +920,6 @@ struct end -type projection = Projection.t - module GlobRefInternal = struct type t = @@ -1015,10 +1010,6 @@ module GlobRef = struct end -type global_reference = GlobRef.t -[@@ocaml.deprecated "Alias for [GlobRef.t]"] - - type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t diff --git a/kernel/names.mli b/kernel/names.mli index 2145a51c4e..37930c12e2 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -527,15 +527,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool (** equalities on constant and inductive names (for the checker) *) -val eq_con_chk : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."] - val eq_ind_chk : inductive -> inductive -> bool -(** {6 Deprecated functions. For backward compatibility.} *) - -type mod_bound_id = MBId.t -[@@ocaml.deprecated "Same as [MBId.t]."] (** {5 Module paths} *) type module_path = ModPath.t = @@ -625,9 +618,6 @@ module Projection : sig end -type projection = Projection.t -[@@ocaml.deprecated "Alias for [Projection.t]"] - (** {6 Global reference is a kernel side type for all references together } *) (* XXX: Should we define GlobRefCan GlobRefUser? *) @@ -665,9 +655,6 @@ module GlobRef : sig end -type global_reference = GlobRef.t -[@@ocaml.deprecated "Alias for [GlobRef.t]"] - (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index b03342da39..820c5b3a2b 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -883,12 +883,6 @@ let typing senv = Typeops.infer (env_of_senv senv) (** {6 Retroknowledge / native compiler } *) -[@@@ocaml.warning "-3"] -(** universal lifting, used for the "get" operations mostly *) -let retroknowledge f senv = - Environ.retroknowledge f (env_of_senv senv) -[@@@ocaml.warning "+3"] - let register field value senv = (* todo : value closed *) (* spiwack : updates the safe_env with the information that the register diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index efb4957006..0f150ea971 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -208,9 +208,6 @@ val delta_of_senv : open Retroknowledge -val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a -[@@ocaml.deprecated "Use the projection of Environ.env"] - val register : field -> GlobRef.t -> safe_transformer0 diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 752bf76270..4336a22b8c 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -12,8 +12,6 @@ open Univ (** {6 Graphs of universes. } *) type t -type universes = t -[@@ocaml.deprecated "Use UGraph.t"] type 'a check_function = t -> 'a -> 'a -> bool diff --git a/kernel/univ.ml b/kernel/univ.ml index 61ad1d0a82..fa37834a23 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -574,11 +574,8 @@ struct pp_std ++ prl u1 ++ pr_constraint_type op ++ prl u2 ++ fnl () ) c (str "") - let universes_of c = - fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end -let universes_of_constraints = Constraint.universes_of let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal @@ -897,8 +894,6 @@ let subst_instance_constraints s csts = (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) csts Constraint.empty -type universe_instance = Instance.t - type 'a puniverses = 'a * Instance.t let out_punivs (x, _y) = x let in_punivs x = (x, Instance.empty) @@ -955,7 +950,6 @@ struct end -type abstract_universe_context = AUContext.t let hcons_abstract_universe_context = AUContext.hcons (** Universe info for cumulative inductive types: A context of @@ -997,12 +991,10 @@ struct end -type cumulativity_info = CumulativityInfo.t let hcons_cumulativity_info = CumulativityInfo.hcons module ACumulativityInfo = CumulativityInfo -type abstract_cumulativity_info = ACumulativityInfo.t let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons (** A set of universes with universe constraints. @@ -1238,7 +1230,3 @@ let explain_universe_inconsistency prl (o,u,v,p) = in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ pr_rel o ++ spc() ++ pr_uni v ++ reason - -let compare_levels = Level.compare -let eq_levels = Level.equal -let equal_universes = Universe.equal diff --git a/kernel/univ.mli b/kernel/univ.mli index b68bbdf359..1aa53b8aa8 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -51,9 +51,6 @@ sig val name : t -> (Names.DirPath.t * int) option end -type universe_level = Level.t -[@@ocaml.deprecated "Use Level.t"] - (** Sets of universe levels *) module LSet : sig @@ -63,9 +60,6 @@ sig (** Pretty-printing *) end -type universe_set = LSet.t -[@@ocaml.deprecated "Use LSet.t"] - module Universe : sig type t @@ -130,9 +124,6 @@ sig end -type universe = Universe.t -[@@ocaml.deprecated "Use Universe.t"] - (** Alias name. *) val pr_uni : Universe.t -> Pp.t @@ -171,9 +162,6 @@ module Constraint : sig include Set.S with type elt = univ_constraint end -type constraints = Constraint.t -[@@ocaml.deprecated "Use Constraint.t"] - val empty_constraint : Constraint.t val union_constraint : Constraint.t -> Constraint.t -> Constraint.t val eq_constraint : Constraint.t -> Constraint.t -> bool @@ -301,9 +289,6 @@ sig end -type universe_instance = Instance.t -[@@ocaml.deprecated "Use Instance.t"] - val enforce_eq_instances : Instance.t constraint_function val enforce_eq_variance_instances : Variance.t array -> Instance.t constraint_function @@ -340,9 +325,6 @@ sig end -type universe_context = UContext.t -[@@ocaml.deprecated "Use UContext.t"] - module AUContext : sig type t @@ -367,9 +349,6 @@ sig end -type abstract_universe_context = AUContext.t -[@@ocaml.deprecated "Use AUContext.t"] - (** Universe info for cumulative inductive types: A context of universe levels with universe constraints, representing local universe variables and constraints, together with an array of @@ -398,9 +377,6 @@ sig val eq_constraints : t -> Instance.t constraint_function end -type cumulativity_info = CumulativityInfo.t -[@@ocaml.deprecated "Use CumulativityInfo.t"] - module ACumulativityInfo : sig type t @@ -411,11 +387,13 @@ sig val eq_constraints : t -> Instance.t constraint_function end -type abstract_cumulativity_info = ACumulativityInfo.t -[@@ocaml.deprecated "Use ACumulativityInfo.t"] - (** Universe contexts (as sets) *) +(** A set of universes with universe Constraint.t. + We linearize the set to a list after typechecking. + Beware, representation could change. +*) + module ContextSet : sig type t = LSet.t constrained @@ -451,13 +429,6 @@ sig val size : t -> int end -(** A set of universes with universe Constraint.t. - We linearize the set to a list after typechecking. - Beware, representation could change. -*) -type universe_context_set = ContextSet.t -[@@ocaml.deprecated "Use ContextSet.t"] - (** A value in a universe context (resp. context set). *) type 'a in_universe_context = 'a * UContext.t type 'a in_universe_context_set = 'a * ContextSet.t @@ -532,20 +503,3 @@ val hcons_abstract_universe_context : AUContext.t -> AUContext.t val hcons_universe_context_set : ContextSet.t -> ContextSet.t val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t - -(******) - -(* deprecated: use qualified names instead *) -val compare_levels : Level.t -> Level.t -> int -[@@ocaml.deprecated "Use Level.compare"] - -val eq_levels : Level.t -> Level.t -> bool -[@@ocaml.deprecated "Use Level.equal"] - -(** deprecated: Equality of formal universe expressions. *) -val equal_universes : Universe.t -> Universe.t -> bool -[@@ocaml.deprecated "Use Universe.equal"] - -(** Universes of Constraint.t *) -val universes_of_constraints : Constraint.t -> LSet.t -[@@ocaml.deprecated "Use Constraint.universes_of"] diff --git a/lib/feedback.ml b/lib/feedback.ml index cb8f8aad1e..9654711ebb 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -84,7 +84,7 @@ let feedback_logger ?loc lvl msg = let msg_info ?loc x = feedback_logger ?loc Info x let msg_notice ?loc x = feedback_logger ?loc Notice x let msg_warning ?loc x = feedback_logger ?loc Warning x -let msg_error ?loc x = feedback_logger ?loc Error x +(* let msg_error ?loc x = feedback_logger ?loc Error x *) let msg_debug ?loc x = feedback_logger ?loc Debug x (* Helper for tools willing to understand only the messages *) diff --git a/lib/feedback.mli b/lib/feedback.mli index 64fdf3724d..f407e2fd5b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -95,11 +95,6 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. *) -val msg_error : ?loc:Loc.t -> Pp.t -> unit -[@@ocaml.deprecated "msg_error is an internal function and should not be \ - used unless you know what you are doing. Use \ - [CErrors.user_err] instead."] - val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) @@ -42,9 +42,6 @@ type doc_view = internal representation opaque here. *) type t = doc_view -type std_ppcmds = t -[@@ocaml.deprecated "alias of Pp.t"] - let repr x = x let unrepr x = x diff --git a/lib/pp.mli b/lib/pp.mli index ed31daa561..4ce6a535c8 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -42,9 +42,6 @@ type pp_tag = string internal representation opaque here. *) type t -type std_ppcmds = t -[@@ocaml.deprecated "alias of Pp.t"] - type block_type = | Pp_hbox of int | Pp_vbox of int diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index d65b35c462..9c421f5b76 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -398,7 +398,6 @@ let set_lexer_state (o,s,b,c,f) = current_file := f let get_lexer_state () = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) -let release_lexer_state = get_lexer_state let drop_lexer_state () = set_lexer_state (init_lexer_state Loc.ToplevelInput) diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index a14f08d91f..e4aa8debc1 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -54,7 +54,5 @@ type lexer_state val init_lexer_state : Loc.source -> lexer_state val set_lexer_state : lexer_state -> unit val get_lexer_state : unit -> lexer_state -val release_lexer_state : unit -> lexer_state -[@@ocaml.deprecated "Use get_lexer_state"] val drop_lexer_state : unit -> unit val get_comment_state : lexer_state -> ((int * int) * string) list diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index c21f8f0d9a..c05229d576 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -23,12 +23,6 @@ module Gram : sig include Grammar.S with type te = Tok.t - type 'a entry = 'a Entry.e - [@@ocaml.deprecated "Use [Pcoq.Entry.t]"] - - val entry_create : string -> 'a Entry.e - [@@ocaml.deprecated "Use [Pcoq.Entry.create]"] - val gram_extend : 'a Entry.e -> 'a Extend.extend_statement -> unit end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 11d13d3a2f..8731cbf60d 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use [Goal_select.t]"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 6b131edaac..9958d6dcda 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e978adf761..bae13dbba1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1386,8 +1386,6 @@ let solve_unif_constraints_with_heuristics env check_problems_are_solved env heuristic_solved_evd; solve_unconstrained_impossible_cases env heuristic_solved_evd -let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics - (* Main entry points *) exception UnableToUnify of evar_map * unification_error @@ -1414,13 +1412,3 @@ let conv env ?(ts=default_transparent_state env) evd t1 t2 = let cumul env ?(ts=default_transparent_state env) evd t1 t2 = make_opt(evar_conv_x ts env evd CUMUL t1 t2) - -let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = - match evar_conv_x ts env !evdref CONV t1 t2 with - | Success evd' -> evdref := evd'; true - | _ -> false - -let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 = - match evar_conv_x ts env !evdref CUMUL t1 t2 with - | Success evd' -> evdref := evd'; true - | _ -> false diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index cdf5dd0e50..20a4f34ec7 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -27,12 +27,6 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma (** The same function resolving evars by side-effect and catching the exception *) -val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool -[@@ocaml.deprecated "Use [Evarconv.conv]"] - -val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool -[@@ocaml.deprecated "Use [Evarconv.cumul]"] - val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option @@ -43,9 +37,6 @@ val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map -val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map -[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"] - (** Check all pending unification problems are solved and raise an error otherwise *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2dd3721980..c0565f4f47 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1690,8 +1690,6 @@ let reconsider_unif_constraints conv_algo evd = (Success evd) pbs -let reconsider_conv_pbs = reconsider_unif_constraints - (* Tries to solve problem t1 = t2. * Precondition: t1 is an uninstantiated evar * Returns an optional list of evars that were instantiated, or None diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 3f05c58c41..4665ed29a2 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -62,9 +62,6 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result -val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result -[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"] - val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0fa573b9a6..ea222397a8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -269,10 +269,6 @@ let allowed_sorts env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_kelim -let projection_nparams_env _ p = Projection.npars p - -let projection_nparams p = Projection.npars p - let has_dependent_elim mib = match mib.mind_record with | PrimRecord _ -> mib.mind_finite == BiFinite diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ea34707bfc..b2e205115f 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -129,15 +129,9 @@ val allowed_sorts : env -> inductive -> Sorts.family list val has_dependent_elim : mutual_inductive_body -> bool (** Primitive projections *) -val projection_nparams : Projection.t -> int -[@@ocaml.deprecated "Use [Projection.npars]"] -val projection_nparams_env : env -> Projection.t -> int -[@@ocaml.deprecated "Use [Projection.npars]"] - val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> EConstr.t -> EConstr.types -> types - (** Extract information from an inductive family *) type constructor_summary = { @@ -152,8 +146,6 @@ val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary val get_constructors : env -> inductive_family -> constructor_summary array -val get_projections : env -> inductive -> Projection.Repr.t array option -[@@ocaml.deprecated "Use [Environ.get_projections]"] (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4ba715f0d5..dc3f042431 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -398,9 +398,6 @@ let check env sigma c t = error_actual_type_core env sigma j t | Some sigma -> sigma -let e_check env evdref c t = - evdref := check env !evdref c t - (* Type of a constr *) let unsafe_type_of env sigma c = @@ -416,9 +413,6 @@ let sort_of env sigma c = let sigma, a = type_judgment env sigma j in sigma, a.utj_type -let e_sort_of env evdref c = - Evarutil.evd_comb1 (sort_of env) evdref c - (* Try to solve the existential variables by typing *) let type_of ?(refresh=false) env sigma c = @@ -429,16 +423,10 @@ let type_of ?(refresh=false) env sigma c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma j.uj_type else sigma, j.uj_type -let e_type_of ?refresh env evdref c = - Evarutil.evd_comb1 (type_of ?refresh env) evdref c - let solve_evars env sigma c = let env = enrich_env env sigma in let sigma, j = execute env sigma c in (* side-effect on evdref *) sigma, nf_evar sigma j.uj_val -let e_solve_evars env evdref c = - Evarutil.evd_comb1 (solve_evars env) evdref c - let _ = Evarconv.set_solve_evars (fun env sigma c -> solve_evars env sigma c) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 3cf43ace01..b8830ff4a2 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -24,27 +24,17 @@ val unsafe_type_of : env -> evar_map -> constr -> types universes *) val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types -(** Variant of [type_of] using references instead of state-passing. *) -val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types -[@@ocaml.deprecated "Use [Typing.type_of]"] - (** Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> evar_map * Sorts.t -val e_sort_of : env -> evar_map ref -> types -> Sorts.t -[@@ocaml.deprecated "Use [Typing.sort_of]"] (** Typecheck a term has a given type (assuming the type is OK) *) val check : env -> evar_map -> constr -> types -> evar_map -val e_check : env -> evar_map ref -> constr -> types -> unit -[@@ocaml.deprecated "Use [Typing.check]"] (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) val solve_evars : env -> evar_map -> constr -> evar_map * constr -val e_solve_evars : env -> evar_map ref -> constr -> constr -[@@ocaml.deprecated "Use [Typing.solve_evars]"] (** Raise an error message if incorrect elimination for this inductive *) (** (first constr is term to match, second is return predicate) *) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 90d2b7abaf..e7f995c84e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -194,7 +194,6 @@ let tag_var = tag Tag.variable sl ++ id let pr_id = Id.print - let pr_name = Name.print let pr_qualid = pr_qualid let pr_patvar = pr_id diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index bca419c9ac..e7f71849a5 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -34,8 +34,6 @@ val pr_sep_com : constr_expr -> Pp.t val pr_id : Id.t -> Pp.t -val pr_name : Name.t -> Pp.t -[@@ocaml.deprecated "alias of Names.Name.print"] val pr_qualid : qualid -> Pp.t val pr_patvar : Pattern.patvar -> Pp.t diff --git a/printing/printer.ml b/printing/printer.ml index 79654da6e7..990bdaad7d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -17,7 +17,6 @@ open Environ open Globnames open Nametab open Evd -open Proof_type open Refiner open Constrextern open Ppconstr @@ -98,20 +97,6 @@ let pr_econstr_env env sigma c = pr_econstr_core false env sigma c let pr_open_lconstr_env env sigma (_,c) = pr_leconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_econstr_env env sigma c -(* NB do not remove the eta-redexes! Global.env() has side-effects... *) -let pr_lconstr t = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_env env sigma t -let pr_constr t = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_env env sigma t - -let pr_leconstr c = pr_lconstr (EConstr.Unsafe.to_constr c) -let pr_econstr c = pr_constr (EConstr.Unsafe.to_constr c) - -let pr_open_lconstr (_,c) = pr_leconstr c -let pr_open_constr (_,c) = pr_econstr c - let pr_constr_under_binders_env_gen pr env sigma (ids,c) = (* Warning: clashes can occur with variables of same name in env but *) (* we also need to preserve the actual names of the patterns *) @@ -122,13 +107,6 @@ let pr_constr_under_binders_env_gen pr env sigma (ids,c) = let pr_constr_under_binders_env = pr_constr_under_binders_env_gen pr_econstr_env let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_leconstr_env -let pr_constr_under_binders c = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_under_binders_env env sigma c -let pr_lconstr_under_binders c = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_under_binders_env env sigma c - let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) let pr_letype_core = Proof_diffs.pr_letype_core @@ -136,13 +114,6 @@ let pr_letype_core = Proof_diffs.pr_letype_core let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) -let pr_ltype t = - let (sigma, env) = Pfedit.get_current_context () in - pr_ltype_env env sigma t -let pr_type t = - let (sigma, env) = Pfedit.get_current_context () in - pr_type_env env sigma t - let pr_etype_env env sigma c = pr_etype_core false env sigma c let pr_letype_env env sigma c = pr_letype_core false env sigma c let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c @@ -150,29 +121,15 @@ let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) -let pr_ljudge j = - let (sigma, env) = Pfedit.get_current_context () in - pr_ljudge_env env sigma j - let pr_lglob_constr_env env c = pr_lconstr_expr (extern_glob_constr (Termops.vars_of_env env) c) let pr_glob_constr_env env c = pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c) -let pr_lglob_constr c = - let (sigma, env) = Pfedit.get_current_context () in - pr_lglob_constr_env env c -let pr_glob_constr c = - let (sigma, env) = Pfedit.get_current_context () in - pr_glob_constr_env env c - let pr_closed_glob_n_env env sigma n c = pr_constr_expr_n n (extern_closed_glob false env sigma c) let pr_closed_glob_env env sigma c = pr_constr_expr (extern_closed_glob false env sigma c) -let pr_closed_glob c = - let (sigma, env) = Pfedit.get_current_context () in - pr_closed_glob_env env sigma c let pr_lconstr_pattern_env env sigma c = pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) sigma c) @@ -182,13 +139,6 @@ let pr_constr_pattern_env env sigma c = let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Names.Id.Set.empty t) -let pr_lconstr_pattern t = - let (sigma, env) = Pfedit.get_current_context () in - pr_lconstr_pattern_env env sigma t -let pr_constr_pattern t = - let (sigma, env) = Pfedit.get_current_context () in - pr_constr_pattern_env env sigma t - let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.Internal.set_print_constr @@ -247,13 +197,6 @@ let safe_gen f env sigma c = let safe_pr_lconstr_env = safe_gen pr_lconstr_env let safe_pr_constr_env = safe_gen pr_constr_env -let safe_pr_lconstr t = - let (sigma, env) = Pfedit.get_current_context () in - safe_pr_lconstr_env env sigma t - -let safe_pr_constr t = - let (sigma, env) = Pfedit.get_current_context () in - safe_pr_constr_env env sigma t let pr_universe_ctx_set sigma c = if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then @@ -889,19 +832,6 @@ let pr_goal_by_id ~proof id = pr_selected_subgoal (pr_id id) sigma g) with Not_found -> user_err Pp.(str "No such goal.") -(* Elementary tactics *) - -let pr_prim_rule = function - | Refine c -> - (** FIXME *) - str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ - Constrextern.with_meta_as_hole pr_constr c - -(* Backwards compatibility *) - -let prterm = pr_lconstr - - (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) diff --git a/printing/printer.mli b/printing/printer.mli index 96db7091a6..f9d1a62895 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -27,13 +27,9 @@ val enable_goal_names_printing : bool ref (** Terms *) val pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val pr_lconstr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_env : env -> evar_map -> constr -> Pp.t -val pr_constr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t @@ -43,19 +39,11 @@ val pr_constr_n_env : env -> evar_map -> Notation_gram.tolerability -> co in case of remaining issues (such as reference not in env). *) val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t -val safe_pr_lconstr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t -val safe_pr_constr : constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_econstr : EConstr.t -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t -val pr_leconstr : EConstr.t -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr_n_env : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t @@ -63,54 +51,30 @@ val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t -val pr_open_constr : open_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t -val pr_open_lconstr : open_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_constr_under_binders : constr_under_binders -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t -val pr_lconstr_under_binders : constr_under_binders -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t val pr_ltype_env : env -> evar_map -> types -> Pp.t -val pr_ltype : types -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_type_env : env -> evar_map -> types -> Pp.t -val pr_type : types -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_closed_glob_n_env : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t -val pr_closed_glob : closed_glob_constr -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t -val pr_lglob_constr : 'a glob_constr_g -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t -val pr_glob_constr : 'a glob_constr_g -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t -val pr_lconstr_pattern : constr_pattern -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t -val pr_constr_pattern : constr_pattern -> Pp.t -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_cases_pattern : cases_pattern -> Pp.t @@ -222,16 +186,8 @@ val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t -val pr_prim_rule : prim_rule -> Pp.t -[@@ocaml.deprecated "[pr_prim_rule] is scheduled to be removed along with the legacy proof engine"] - val print_and_diff : Proof.t option -> Proof.t option -> unit -(** Backwards compatibility *) - -val prterm : constr -> Pp.t (** = pr_lconstr *) -[@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] - (** Declarations for the "Print Assumption" command *) type axiom = | Constant of Constant.t (* An axiom or a constant. *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 8bbd82bb0a..70a08e4966 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -122,8 +122,6 @@ type t = { initial_euctx : UState.t } -type proof = t - (*** General proof functions ***) let proof p = @@ -435,9 +433,6 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct - let subgoals p = - let it, sigma = Proofview.proofview p.proofview in - Evd.{ it; sigma } let background_subgoals p = let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in diff --git a/proofs/proof.mli b/proofs/proof.mli index 511dcc2e00..8cf543557b 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -33,8 +33,6 @@ (* Type of a proof. *) type t -type proof = t -[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -192,8 +190,6 @@ val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : t -> Goal.goal list Evd.sigma - [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : t -> Goal.goal list Evd.sigma diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index cc3e79f858..ed8df29d7b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -197,6 +197,3 @@ let put p b = let suggest p = (!current_behavior).suggest p - -let pr_goal_selector = Goal_select.pr_goal_selector -let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index a09a7ec1d2..0fcc647a6f 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -44,9 +44,3 @@ val register_behavior : behavior -> unit *) val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t - -(** Deprecated *) -val pr_goal_selector : Goal_select.t -> Pp.t -[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] -val get_default_goal_selector : unit -> Goal_select.t -[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 7e250faa86..de151fb6e5 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -101,7 +101,6 @@ type pstate = { } type t = pstate list -type state = t let make_terminator f = f let apply_terminator f = f diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 854ceaa41a..2b04bfab57 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,8 +13,6 @@ environment. *) type t -type state = t -[@@ocaml.deprecated "please use [Proof_global.t]"] val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1350da65dc..56ce744bc1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -15,7 +15,6 @@ open Names open Constr open EConstr open Declarations -open Globnames open Genredexpr open Pattern open Reductionops @@ -79,7 +78,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () @@ -115,7 +114,7 @@ let classify_strategy (local,_ as obj) = let disch_ref ref = match ref with EvalConstRef c -> Some ref - | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref + | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref let discharge_strategy (_,(local,obj)) = if local then None else diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 0f83e16ec8..30af6d8e1a 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -22,14 +22,6 @@ val project : 'a sigma -> evar_map val pf_env : goal sigma -> Environ.env val pf_hyps : goal sigma -> named_context -val unpackage : 'a sigma -> evar_map ref * 'a -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val repackage : evar_map ref -> 'a -> 'a sigma -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val apply_sig_tac : - evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list -[@@ocaml.deprecated "Do not use [evar_map ref]"] - val refiner : rule -> tactic (** {6 Tacticals. } *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 9e42a71ea8..5d1faf1465 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -30,14 +30,7 @@ let re_sig it gc = { it = it; sigma = gc; } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Evd.sigma;; -type tactic = Proof_type.tactic;; - -[@@@ocaml.warning "-3"] -let unpackage = Refiner.unpackage -let repackage = Refiner.repackage -let apply_sig_tac = Refiner.apply_sig_tac -[@@@ocaml.warning "+3"] +type tactic = Proof_type.tactic let sig_it = Refiner.sig_it let project = Refiner.project diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index b4cb2be2b8..3432ad4afa 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -18,9 +18,6 @@ open Locus (** Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Evd.sigma -[@@ocaml.deprecated "alias of Evd.sigma"] - open Evd type tactic = Proof_type.tactic;; @@ -29,14 +26,6 @@ val project : goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val unpackage : 'a sigma -> evar_map ref * 'a -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val repackage : evar_map ref -> 'a -> 'a sigma -[@@ocaml.deprecated "Do not use [evar_map ref]"] -val apply_sig_tac : - evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) -[@@ocaml.deprecated "Do not use [evar_map ref]"] - val pf_concl : goal sigma -> types val pf_env : goal sigma -> env val pf_hyps : goal sigma -> named_context diff --git a/tactics/hints.ml b/tactics/hints.ml index 90eafe88c4..af6d1c472f 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1552,11 +1552,6 @@ let pr_hint_db_env env sigma db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content -(* Deprecated in the mli *) -let pr_hint_db db = - let sigma, env = Pfedit.get_current_context () in - pr_hint_db_env env sigma db - let pr_hint_db_by_name env sigma dbname = try let db = searchtable_map dbname in pr_hint_db_env env sigma db diff --git a/tactics/hints.mli b/tactics/hints.mli index d63efea27d..6db8feccd0 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -298,9 +298,4 @@ val pr_applicable_hint : unit -> Pp.t val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t -val pr_hint_db : Hint_db.t -> Pp.t -[@@ocaml.deprecated "please used pr_hint_db_env"] val pr_hint : env -> evar_map -> hint -> Pp.t - -type nonrec hint_info = hint_info -[@@ocaml.deprecated "Use [Typeclasses.hint_info]"] diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 596feeec8b..f2cf915fe3 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -60,10 +60,6 @@ let tclIFTHENSELSE = Refiner.tclIFTHENSELSE let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST -(* Synonyms *) - -let tclTHENSEQ = tclTHENLIST - (************************************************************************) (* Tacticals applying on hypotheses *) (************************************************************************) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 1e66c2b0b1..cc15469d0e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -23,8 +23,6 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic -val tclTHENSEQ : tactic list -> tactic -[@@ocaml.deprecated "alias of Tacticals.tclTHENLIST"] val tclTHENLIST : tactic list -> tactic val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclTHENFIRST : tactic -> tactic -> tactic diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index aa9bd20bf3..4f0bf1b5d2 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -533,7 +533,3 @@ let save_proof ?proof = function (* if the proof is given explicitly, nothing has to be deleted *) if Option.is_empty proof then Proof_global.discard_current (); Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) - -(* Miscellaneous *) -let get_current_context () = Pfedit.get_current_context () - diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 38683ed6b2..62b25946d9 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -67,10 +67,3 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val val set_save_hook : (Proof.t -> unit) -> unit val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - -(** [get_current_context ()] returns the evar context and env of the - current open proof if any, otherwise returns the empty evar context - and the current global env *) - -val get_current_context : unit -> Evd.evar_map * Environ.env -[@@ocaml.deprecated "please use [Pfedit.get_current_context]"] diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml deleted file mode 100644 index ef9cd3c351..0000000000 --- a/vernac/misctypes.ml +++ /dev/null @@ -1,75 +0,0 @@ -(* Compat module, to be removed in 8.10 *) -open Names - -type lident = Names.lident -[@@ocaml.deprecated "use [Names.lident"] -type lname = Names.lname -[@@ocaml.deprecated "use [Names.lname]"] -type lstring = Names.lstring -[@@ocaml.deprecated "use [Names.lstring]"] - -type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r = - | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"] - | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"] -[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"] - -type 'a or_by_notation = 'a Constrexpr.or_by_notation -[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"] - -type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr = - | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Namegen]"] - | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"] - | IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"] -[@@ocaml.deprecated "use [Namegen.intro_pattern_naming_expr]"] - -type 'a or_var = 'a Locus.or_var = - | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"] - | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"] -[@@ocaml.deprecated "use [Locus.or_var]"] - -type quantified_hypothesis = Tactypes.quantified_hypothesis = - AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"] - | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"] -[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"] - -type multi = Equality.multi = - | Precisely of int [@ocaml.deprecated "use version in [Equality]"] - | UpTo of int [@ocaml.deprecated "use version in [Equality]"] - | RepeatStar [@ocaml.deprecated "use version in [Equality]"] - | RepeatPlus [@ocaml.deprecated "use version in [Equality]"] -[@@ocaml.deprecated "use [Equality.multi]"] - -type 'a bindings = 'a Tactypes.bindings = - | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"] - | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"] - | NoBindings [@ocaml.deprecated "use version in [Tactypes]"] -[@@ocaml.deprecated "use [Tactypes.bindings]"] - -type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr = - | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"] - | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"] - | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"] -and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr = - | IntroWildcard [@ocaml.deprecated "use [Tactypes]"] - | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"] - | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"] - | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"] - | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"] -and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr = - | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"] - | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"] -[@@ocaml.deprecated "use version in [Tactypes]"] - -type 'id move_location = 'id Logic.move_location = - | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"] - | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"] - | MoveFirst [@ocaml.deprecated "use version in [Logic]"] - | MoveLast [@ocaml.deprecated "use version in [Logic]"] -[@@ocaml.deprecated "use version in [Logic]"] - -type 'a cast_type = 'a Glob_term.cast_type = - | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"] - | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"] - | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"] - | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"] -[@@ocaml.deprecated "use version in [Glob_term]"] diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index a5601d8c85..a2ea706b75 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -15,14 +15,6 @@ open Libnames (** Vernac expressions, produced by the parser *) type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation -type goal_selector = Goal_select.t = - | SelectAlreadyFocused [@ocaml.deprecated "Use Goal_select.SelectAlreadyFocused"] - | SelectNth of int [@ocaml.deprecated "Use Goal_select.SelectNth"] - | SelectList of (int * int) list [@ocaml.deprecated "Use Goal_select.SelectList"] - | SelectId of Id.t [@ocaml.deprecated "Use Goal_select.SelectId"] - | SelectAll [@ocaml.deprecated "Use Goal_select.SelectAll"] -[@@ocaml.deprecated "Use Goal_select.t"] - type goal_identifier = string type scope_name = string @@ -31,9 +23,6 @@ type goal_reference = | NthGoal of int | GoalId of Id.t -type univ_name_list = UnivNames.univ_name_list -[@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] - type printable = | PrintTables | PrintFullContext @@ -102,54 +91,12 @@ type comment = | CommentString of string | CommentInt of int -type reference_or_constr = Hints.reference_or_constr = - | HintsReference of qualid [@ocaml.deprecated "Use Hints.HintsReference"] - | HintsConstr of constr_expr [@ocaml.deprecated "Use Hints.HintsConstr"] -[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"] - -type hint_mode = Hints.hint_mode = - | ModeInput [@ocaml.deprecated "Use Hints.ModeInput"] - | ModeNoHeadEvar [@ocaml.deprecated "Use Hints.ModeNoHeadEvar"] - | ModeOutput [@ocaml.deprecated "Use Hints.ModeOutput"] -[@@ocaml.deprecated "Please use [Hints.hint_mode]"] - -type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = - { hint_priority : int option; [@ocaml.deprecated "Use Typeclasses.hint_priority"] - hint_pattern : 'a option [@ocaml.deprecated "Use Typeclasses.hint_pattern"] } -[@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] - -type hint_info_expr = Hints.hint_info_expr -[@@ocaml.deprecated "Please use [Hints.hint_info_expr]"] - -type hints_expr = Hints.hints_expr = - | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsResolveIFF of bool * qualid list * int option - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsImmediate of Hints.reference_or_constr list - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsUnfold of qualid list - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsTransparency of qualid Hints.hints_transparency_target * bool - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsMode of qualid * Hints.hint_mode list - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsConstructors of qualid list - [@ocaml.deprecated "Use the constructor in module [Hints]"] - | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument - [@ocaml.deprecated "Use the constructor in module [Hints]"] -[@@ocaml.deprecated "Please use [Hints.hints_expr]"] - type search_restriction = | SearchInside of qualid list | SearchOutside of qualid list type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Proof_global.opacity_flag = - Opaque [@ocaml.deprecated "Use Proof_global.Opaque"] - | Transparent [@ocaml.deprecated "Use Proof_global.Transparent"] - [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) @@ -285,33 +232,8 @@ type register_kind = | RegisterInline | RegisterRetroknowledge of qualid -type bullet = Proof_bullet.t -[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"] - (** {6 Types concerning the module layer} *) -(** Rigid / flexible module signature *) - -type 'a module_signature = 'a Declaremods.module_signature = - | Enforce of 'a (** ... : T *) - [@ocaml.deprecated "Use the constructor in module [Declaremods]"] - | Check of 'a list (** ... <: T1 <: T2, possibly empty *) - [@ocaml.deprecated "Use the constructor in module [Declaremods]"] -[@@ocaml.deprecated "please use [Declaremods.module_signature]."] - -(** Which module inline annotations should we honor, - either None or the ones whose level is less or equal - to the given integer *) - -type inline = Declaremods.inline = - | NoInline - [@ocaml.deprecated "Use the constructor in module [Declaremods]"] - | DefaultInline - [@ocaml.deprecated "Use the constructor in module [Declaremods]"] - | InlineAt of int - [@ocaml.deprecated "Use the constructor in module [Declaremods]"] -[@@ocaml.deprecated "please use [Declaremods.inline]."] - type module_ast_inl = module_ast * Declaremods.inline type module_binder = bool option * lident list * module_ast_inl |