aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/texmacspp.ml2
-rw-r--r--interp/smartlocate.ml6
-rw-r--r--interp/stdarg.ml2
-rw-r--r--intf/genredexpr.mli2
-rw-r--r--intf/misctypes.mli12
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--parsing/g_prim.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml10
-rw-r--r--plugins/ltac/g_tactic.ml44
-rw-r--r--plugins/ltac/pptactic.ml10
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/ltac/tacinterp.ml6
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--pretyping/miscops.ml2
-rw-r--r--printing/pputils.ml2
-rw-r--r--printing/prettyp.ml4
-rw-r--r--proofs/clenv.ml6
-rw-r--r--vernac/vernacentries.ml4
21 files changed, 47 insertions, 49 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 77dca0d06..f86b260df 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -649,7 +649,7 @@ let rec tmpp v loc =
match r with
| AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
| AN (Ident (_, id)) -> ["id", Id.to_string id]
- | ByNotation (_, s, _) -> ["notation", s] in
+ | ByNotation (_, (s, _)) -> ["notation", s] in
xmlCanonicalStructure attr loc
| VernacCoercion _ as x -> xmlTODO loc x
| VernacIdentityCoercion _ as x -> xmlTODO loc x
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index d863e0561..64d260cc1 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -66,16 +66,16 @@ let global_with_alias ?head r =
let smart_global ?head = function
| AN r ->
global_with_alias ?head r
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
let smart_global_inductive = function
| AN r ->
global_inductive_with_alias r
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
destIndRef
(Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
let loc_of_smart_reference = function
| AN r -> loc_of_reference r
- | ByNotation (loc,_,_) -> loc
+ | ByNotation (loc,(_,_)) -> loc
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662..c0dd9e45c 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,7 +34,7 @@ let wit_pre_ident : string uniform_genarg_type =
let loc_of_or_by_notation f = function
| AN c -> f c
- | ByNotation (loc,s,_) -> loc
+ | ByNotation (loc,(s,_)) -> loc
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 16f0c0c92..2a542e0ff 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen =
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
| ConstrEval of ('a,'b,'c) red_expr_gen * 'a
- | ConstrContext of (Loc.t * Id.t) * 'a
+ | ConstrContext of Id.t Loc.located * 'a
| ConstrTypeOf of 'a
open Libnames
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 33dc2a335..0157800cd 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -27,12 +27,12 @@ and intro_pattern_naming_expr =
and 'constr intro_pattern_action_expr =
| IntroWildcard
| IntroOrAndPattern of 'constr or_and_intro_pattern_expr
- | IntroInjection of (Loc.t * 'constr intro_pattern_expr) list
- | IntroApplyOn of (Loc.t * 'constr) * (Loc.t * 'constr intro_pattern_expr)
+ | IntroInjection of ('constr intro_pattern_expr) Loc.located list
+ | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
| IntroRewrite of bool
and 'constr or_and_intro_pattern_expr =
- | IntroOrPattern of (Loc.t * 'constr intro_pattern_expr) list list
- | IntroAndPattern of (Loc.t * 'constr intro_pattern_expr) list
+ | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list
+ | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list
(** Move destination for hypothesis *)
@@ -79,7 +79,7 @@ type 'a cast_type =
type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
-type 'a explicit_bindings = (Loc.t * quantified_hypothesis * 'a) list
+type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list
type 'a bindings =
| ImplicitBindings of 'a list
@@ -99,7 +99,7 @@ type 'a and_short_name = 'a * Id.t Loc.located option
type 'a or_by_notation =
| AN of 'a
- | ByNotation of (Loc.t * string * string option)
+ | ByNotation of (string * string option) Loc.located
(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
but this formulation avoids a useless dependency. *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f018d59e6..211d41bb0 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -482,7 +482,7 @@ and vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
and vernac_argument_status = {
name : Name.t;
recarg_like : bool;
- notation_scope : (Loc.t * string) option;
+ notation_scope : string Loc.located option;
implicit_status : vernac_implicit_status;
}
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 2af4ed533..ed6a8df4e 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -81,7 +81,7 @@ GEXTEND Gram
] ]
;
by_notation:
- [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (!@loc, s, sc) ] ]
+ [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> Loc.tag ~loc:!@loc (s, sc) ] ]
;
smart_global:
[ [ c = reference -> Misctypes.AN c
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 4248db697..959e8ddf5 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -206,7 +206,7 @@ module Prim :
val qualid : qualid located Gram.entry
val fullyqualid : Id.t list located Gram.entry
val reference : reference Gram.entry
- val by_notation : (Loc.t * string * string option) Gram.entry
+ val by_notation : (string * string option) Loc.located Gram.entry
val smart_global : reference or_by_notation Gram.entry
val dirpath : DirPath.t Gram.entry
val ne_string : string Gram.entry
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dccd25d7..129c8dc16 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -24,8 +24,8 @@ open Pltac
DECLARE PLUGIN "recdef_plugin"
let pr_binding prc = function
- | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+ | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
let pr_bindings prc prlc = function
| ImplicitBindings l ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898..8da4f9233 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -31,8 +31,8 @@ module RelDecl = Context.Rel.Declaration
let pr_binding prc =
function
- | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
let pr_bindings prc prlc = function
| ImplicitBindings l ->
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c796fe7a2..25daedd0e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -882,9 +882,8 @@ let rec make_rewrite_list expr_info max = function
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
(mkVar hp,
- ExplicitBindings[Loc.ghost,NamedHyp def,
- expr_info.f_constr;Loc.ghost,NamedHyp k,
- f_S max]) false) g) )
+ ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
+ Loc.tag @@ (NamedHyp k, f_S max)]) false) g) )
)
[make_rewrite_list expr_info max l;
observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -910,9 +909,8 @@ let make_rewrite expr_info l hp max =
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
(mkVar hp,
- ExplicitBindings[Loc.ghost,NamedHyp def,
- expr_info.f_constr;Loc.ghost,NamedHyp k,
- f_S (f_S max)]) false)) g)
+ ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
+ Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g)
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1674bb4ca..d1e5c810f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -336,8 +336,8 @@ GEXTEND Gram
| pat = naming_intropattern -> !@loc, IntroNaming pat ] ]
;
simple_binding:
- [ [ "("; id = ident; ":="; c = lconstr; ")" -> (!@loc, NamedHyp id, c)
- | "("; n = natural; ":="; c = lconstr; ")" -> (!@loc, AnonHyp n, c) ] ]
+ [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c)
+ | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ]
;
bindings:
[ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index aec2e37fd..0dd6819fd 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -149,7 +149,7 @@ type 'a extra_genarg_printer =
let pr_or_by_notation f = function
| AN v -> f v
- | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+ | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let pr_located pr (loc,x) = pr x
@@ -162,8 +162,8 @@ type 'a extra_genarg_printer =
| NamedHyp id -> pr_id id
let pr_binding prc = function
- | loc, NamedHyp id, c -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+ | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
+ | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
let pr_bindings prc prlc = function
| ImplicitBindings l ->
@@ -368,8 +368,8 @@ type 'a extra_genarg_printer =
let pr_esubst prc l =
let pr_qhyp = function
- (_,AnonHyp n,c) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
- | (_,NamedHyp id,c) ->
+ (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
+ | (_,(NamedHyp id,c)) ->
str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
in
prlist_with_sep spc pr_qhyp l
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e7d4c1be9..ad9814b84 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -212,8 +212,8 @@ let intern_constr = intern_constr_gen false false
let intern_type = intern_constr_gen false true
(* Globalize bindings *)
-let intern_binding ist (loc,b,c) =
- (loc,intern_binding_name ist b,intern_constr ist c)
+let intern_binding ist (loc,(b,c)) =
+ (loc,(intern_binding_name ist b,intern_constr ist c))
let intern_bindings ist = function
| NoBindings -> NoBindings
@@ -291,7 +291,7 @@ let intern_evaluable_global_reference ist r =
let intern_evaluable_reference_or_by_notation ist = function
| AN r -> intern_evaluable_global_reference ist r
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
evaluable_of_global_reference ist.genv
(Notation.interp_notation_as_global_reference loc
(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a8d8eda1d..aac63fcb2 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -987,9 +987,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
(coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id)
with Not_found -> NamedHyp id
-let interp_binding ist env sigma (loc,b,c) =
+let interp_binding ist env sigma (loc,(b,c)) =
let sigma, c = interp_open_constr ist env sigma c in
- sigma, (loc,interp_binding_name ist sigma b,c)
+ sigma, (loc,(interp_binding_name ist sigma b,c))
let interp_bindings ist env sigma = function
| NoBindings ->
@@ -1014,7 +1014,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
let loc_of_bindings = function
| NoBindings -> Loc.ghost
| ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
-| ExplicitBindings l -> pi1 (List.last l)
+| ExplicitBindings l -> fst (List.last l)
let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
let loc1 = loc_of_glob_constr c in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index fe3a9f3b2..9582ebd89 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -32,8 +32,8 @@ let subst_glob_constr_and_expr subst (c, e) =
let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
-let subst_binding subst (loc,b,c) =
- (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c)
+let subst_binding subst (loc,(b,c)) =
+ (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c))
let subst_bindings subst = function
| NoBindings -> NoBindings
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 7fe81c9a4..f53677abb 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -62,7 +62,7 @@ let map_red_expr_gen f g h = function
(** Mapping bindings *)
let map_explicit_bindings f l =
- let map (loc, hyp, x) = (loc, hyp, f x) in
+ let map (loc, (hyp, x)) = (loc, (hyp, f x)) in
List.map map l
let map_bindings f = function
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 50630fb9b..e90b54685 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -105,7 +105,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
let pr_or_by_notation f = function
| AN v -> f v
- | ByNotation (_,s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+ | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index aa422e36a..96b0f49d4 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -750,7 +750,7 @@ let print_any_name = function
~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
let print_name = function
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
print_any_name
(Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
ntn sc))
@@ -798,7 +798,7 @@ let print_about_any loc k =
hov 0 (pr_located_qualid k)
let print_about = function
- | ByNotation (loc,ntn,sc) ->
+ | ByNotation (loc,(ntn,sc)) ->
print_about_any loc
(Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
ntn sc))
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f9ebc4233..17a9651cd 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -421,7 +421,7 @@ let qhyp_eq h1 h2 = match h1, h2 with
| _ -> false
let check_bindings bl =
- match List.duplicates qhyp_eq (List.map pi2 bl) with
+ match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
| NamedHyp s :: _ ->
user_err
(str "The variable " ++ pr_id s ++
@@ -517,7 +517,7 @@ let clenv_match_args bl clenv =
let mvs = clenv_independent clenv in
check_bindings bl;
List.fold_left
- (fun clenv (loc,b,c) ->
+ (fun clenv (loc,(b,c)) ->
let k = meta_of_binder clenv loc mvs b in
if meta_defined clenv.evd k then
if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
@@ -716,7 +716,7 @@ let solve_evar_clause env sigma hyp_only clause = function
error_not_right_number_missing_arguments len
| ExplicitBindings lbind ->
let () = check_bindings lbind in
- let fold sigma (_, binder, c) =
+ let fold sigma (_, (binder, c)) =
let ev = evar_of_binder clause.cl_holes binder in
define_with_type sigma env ev c
in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0a5a000fe..86406dbe5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1772,8 +1772,8 @@ let vernac_search ~loc s gopt r =
let vernac_locate = let open Feedback in function
| LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
| LocateTerm (AN qid) -> msg_notice (print_located_term qid)
- | LocateAny (ByNotation (_, ntn, sc)) (** TODO : handle Ltac notations *)
- | LocateTerm (ByNotation (_, ntn, sc)) ->
+ | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
+ | LocateTerm (ByNotation (_, (ntn, sc))) ->
msg_notice
(Notation.locate_notation
(Constrextern.without_symbols pr_lglob_constr) ntn sc)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 16:45:18 +0000