aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml8
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comAssumption.ml5
-rw-r--r--vernac/comFixpoint.ml10
-rw-r--r--vernac/g_vernac.mlg16
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/lemmas.mli7
-rw-r--r--vernac/misctypes.ml75
-rw-r--r--vernac/vernacentries.ml3
-rw-r--r--vernac/vernacexpr.ml78
10 files changed, 26 insertions, 182 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index b000745961..15c0278f47 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -119,7 +119,7 @@ and fields_of_expression x = fields_of_functor fields_of_expr x
let lookup_constant_in_impl cst fallback =
try
- let mp,dp,lab = KerName.repr (Constant.canonical cst) in
+ let mp,lab = KerName.repr (Constant.canonical cst) in
let fields = memoize_fields_of_mp mp in
(* A module found this way is necessarily closed, in particular
our constant cannot be in an opened section : *)
@@ -143,7 +143,7 @@ let lookup_constant cst =
let lookup_mind_in_impl mind =
try
- let mp,dp,lab = KerName.repr (MutInd.canonical mind) in
+ let mp,lab = KerName.repr (MutInd.canonical mind) in
let fields = memoize_fields_of_mp mp in
search_mind_label lab fields
with Not_found ->
@@ -157,9 +157,9 @@ let lookup_mind mind =
traversed objects *)
let label_of = function
- | ConstRef kn -> pi3 (Constant.repr3 kn)
+ | ConstRef kn -> Constant.label kn
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> pi3 (MutInd.repr3 kn)
+ | ConstructRef ((kn,_),_) -> MutInd.label kn
| VarRef id -> Label.of_id id
let fold_constr_with_full_binders g f n acc c =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c738d14af9..37ee33b19f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -99,7 +99,7 @@ let type_ctx_instance env sigma ctx inst subst =
let id_of_class cl =
match cl.cl_impl with
- | ConstRef kn -> let _,_,l = Constant.repr3 kn in Label.to_id l
+ | ConstRef kn -> Label.to_id @@ Constant.label kn
| IndRef (kn,i) ->
let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
mip.(0).Declarations.mind_typename
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 750ed35cbc..9497f2fb03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -84,8 +84,7 @@ match local with
in
(gr,inst,Lib.is_modtype_strict ())
-let interp_assumption sigma env impls bl c =
- let c = mkCProdN ?loc:(local_binders_loc bl) bl c in
+let interp_assumption sigma env impls c =
let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
sigma, (ty, impls)
@@ -148,7 +147,7 @@ let do_assumptions kind nl l =
in
(* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
- let sigma,(t,imps) = interp_assumption sigma env ienv [] c in
+ let sigma,(t,imps) = interp_assumption sigma env ienv c in
let env =
EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
let ienv = List.fold_right (fun {CAst.v=id} ienv ->
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 37258c2d45..04cd4173a8 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * 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 Pp
open CErrors
open Util
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index cf69a84b8b..895737b538 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
{ if List.exists (function CLocalPattern _ -> true | _ -> false) bl
then
(* FIXME: "red" will be applied to types in bl and Cast with remain *)
- let c = mkCLambdaN ~loc bl c in
+ let c = mkLambdaCN ~loc bl c in
DefineBody ([], red, c, None)
else
(match c with
@@ -308,7 +308,7 @@ GRAMMAR EXTEND Gram
then
(* FIXME: "red" will be applied to types in bl and Cast with remain *)
let c = CAst.make ~loc @@ CCast (c, CastConv t) in
- (([],mkCLambdaN ~loc bl c), None)
+ (([],mkLambdaCN ~loc bl c), None)
else ((bl, c), Some t)
in
DefineBody (bl, red, c, tyo) }
@@ -419,16 +419,16 @@ GRAMMAR EXTEND Gram
;
record_binder_body:
[ [ l = binders; oc = of_type_with_opt_coercion;
- t = lconstr -> { fun id -> (oc,AssumExpr (id,mkCProdN ~loc l t)) }
+ t = lconstr -> { fun id -> (oc,AssumExpr (id,mkProdCN ~loc l t)) }
| l = binders; oc = of_type_with_opt_coercion;
t = lconstr; ":="; b = lconstr -> { fun id ->
- (oc,DefExpr (id,mkCLambdaN ~loc l b,Some (mkCProdN ~loc l t))) }
+ (oc,DefExpr (id,mkLambdaCN ~loc l b,Some (mkProdCN ~loc l t))) }
| l = binders; ":="; b = lconstr -> { fun id ->
match b.CAst.v with
| CCast(b', (CastConv t|CastVM t|CastNative t)) ->
- (None,DefExpr(id,mkCLambdaN ~loc l b',Some (mkCProdN ~loc l t)))
+ (None,DefExpr(id,mkLambdaCN ~loc l b',Some (mkProdCN ~loc l t)))
| _ ->
- (None,DefExpr(id,mkCLambdaN ~loc l b,None)) } ] ]
+ (None,DefExpr(id,mkLambdaCN ~loc l b,None)) } ] ]
;
record_binder:
[ [ id = name -> { (None,AssumExpr(id, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) }
@@ -448,9 +448,9 @@ GRAMMAR EXTEND Gram
constructor_type:
[[ l = binders;
t= [ coe = of_type_with_opt_coercion; c = lconstr ->
- { fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc l c)) }
+ { fun l id -> (not (Option.is_empty coe),(id,mkProdCN ~loc l c)) }
| ->
- { fun l id -> (false,(id,mkCProdN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
+ { fun l id -> (false,(id,mkProdCN ~loc l (CAst.make ~loc @@ CHole (None, IntroAnonymous, None)))) } ]
-> { t l }
]]
;
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/vernacentries.ml b/vernac/vernacentries.ml
index 015d5fabef..cf2fecb9c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -249,8 +249,7 @@ let print_namespace ns =
in
let print_list pr l = prlist_with_sep (fun () -> str".") pr l in
let print_kn kn =
- (* spiwack: I'm ignoring the dirpath, is that bad? *)
- let (mp,_,lbl) = Names.KerName.repr kn in
+ let (mp,lbl) = Names.KerName.repr kn in
let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in
print_list Id.print qn
in
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:04:13 +0000