aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
8 files changed, 23 insertions, 25 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 17:53:56 +0000