aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/rtauto/Bintree.v8
-rw-r--r--plugins/setoid_ring/Field_theory.v4
-rw-r--r--plugins/setoid_ring/Ring_polynom.v4
-rw-r--r--plugins/ssr/ssrbool.v38
-rw-r--r--plugins/ssr/ssrvernac.mlg4
-rw-r--r--plugins/ssrmatching/ssrmatching.ml2
10 files changed, 36 insertions, 34 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
raise NoChange;
end
in
- let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+ let eq_constr c1 c2 =
+ try ignore(Evarconv.unify_delay env sigma c1 c2); true
+ with Evarconv.UnableToUnify _ -> false in
if not (noccurn sigma 1 end_of_type)
then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *)
if not (isApp sigma t) then nochange "not an equality";
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2d833a2cde..e78d0f93a4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
unsolvable constraints remain, so we check that this unification
does not introduce any new problem. *)
let _, pbs = Evd.extract_all_conv_pbs evd in
- let evd' = Evarconv.the_conv_x env x y evd in
+ let evd' = Evarconv.unify_delay env evd x y in
let _, pbs' = Evd.extract_all_conv_pbs evd' in
if evd' == evd || problem_inclusion pbs' pbs then Some evd'
else None
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index a1e21aab04..543d4de0fe 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -557,7 +557,7 @@ let rec intern_atomic lf ist x =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
TacChange (None,
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 30f716d764..eac84f0543 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| _ -> false
in
let is_onconcl = match cl.concl_occs with
- | AllOccurrences | NoOccurrences -> true
+ | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true
| _ -> false
in
let c_interp patvars env sigma =
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 751f0d8334..c2dec264ad 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -294,10 +294,10 @@ Qed.
End Store.
-Arguments PNone [A].
+Arguments PNone {A}.
Arguments PSome [A] _.
-Arguments Tempty [A].
+Arguments Tempty {A}.
Arguments Branch0 [A] _ _.
Arguments Branch1 [A] _ _ _.
@@ -311,7 +311,7 @@ Arguments mkStore [A] index contents.
Arguments index [A] s.
Arguments contents [A] s.
-Arguments empty [A].
+Arguments empty {A}.
Arguments get [A] i S.
Arguments push [A] a S.
@@ -319,7 +319,7 @@ Arguments get_empty [A] i.
Arguments get_push_Full [A] i a S _.
Arguments Full [A] _.
-Arguments F_empty [A].
+Arguments F_empty {A}.
Arguments F_push [A] a S _.
Arguments In [A] x S F.
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index dba72337b2..f5d13053b1 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1789,5 +1789,5 @@ End Field.
End Complete.
-Arguments FEO [C].
-Arguments FEI [C].
+Arguments FEO {C}.
+Arguments FEI {C}.
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 9ef24144d2..12f716c496 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1507,5 +1507,5 @@ Qed.
End MakeRingPol.
-Arguments PEO [C].
-Arguments PEI [C].
+Arguments PEO {C}.
+Arguments PEI {C}.
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index ed4ff2aa66..d6b7371647 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -813,21 +813,21 @@ Proof. by case b1; case b2; constructor; auto. Qed.
End ReflectConnectives.
-Arguments idP [b1].
-Arguments idPn [b1].
-Arguments negP [b1].
-Arguments negPn [b1].
-Arguments negPf [b1].
-Arguments andP [b1 b2].
-Arguments and3P [b1 b2 b3].
-Arguments and4P [b1 b2 b3 b4].
-Arguments and5P [b1 b2 b3 b4 b5].
-Arguments orP [b1 b2].
-Arguments or3P [b1 b2 b3].
-Arguments or4P [b1 b2 b3 b4].
-Arguments nandP [b1 b2].
-Arguments norP [b1 b2].
-Arguments implyP [b1 b2].
+Arguments idP {b1}.
+Arguments idPn {b1}.
+Arguments negP {b1}.
+Arguments negPn {b1}.
+Arguments negPf {b1}.
+Arguments andP {b1 b2}.
+Arguments and3P {b1 b2 b3}.
+Arguments and4P {b1 b2 b3 b4}.
+Arguments and5P {b1 b2 b3 b4 b5}.
+Arguments orP {b1 b2}.
+Arguments or3P {b1 b2 b3}.
+Arguments or4P {b1 b2 b3 b4}.
+Arguments nandP {b1 b2}.
+Arguments norP {b1 b2}.
+Arguments implyP {b1 b2}.
Prenex Implicits idP idPn negP negPn negPf.
Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
@@ -953,7 +953,7 @@ Proof. by case: a; case: b. Qed.
Lemma addbP a b : reflect (~~ a = b) (a (+) b).
Proof. by case: a; case: b; constructor. Qed.
-Arguments addbP [a b].
+Arguments addbP {a b}.
(**
Resolution tactic for blindly weeding out common terms from boolean
@@ -1158,8 +1158,8 @@ Definition clone_pred U :=
End Predicates.
-Arguments pred0 [T].
-Arguments predT [T].
+Arguments pred0 {T}.
+Arguments predT {T}.
Prenex Implicits pred0 predT predI predU predC predD preim relU.
Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B))
@@ -1357,7 +1357,7 @@ Variant qualifier (q : nat) T := Qualifier of predPredType T.
Coercion has_quality n T (q : qualifier n T) : pred_class :=
fun x => let: Qualifier _ p := q in p x.
-Arguments has_quality n [T].
+Arguments has_quality n {T}.
Lemma qualifE n T p x : (x \in @Qualifier n T p) = p x. Proof. by []. Qed.
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d083d34b52..2e1554d496 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -152,7 +152,7 @@ let declare_one_prenex_implicit locality f =
with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
let rec loop = function
| a :: args' when Impargs.is_status_implicit a ->
- (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args'
+ Impargs.MaximallyImplicit :: loop args'
| args' when List.exists Impargs.is_status_implicit args' ->
errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
| _ -> [] in
@@ -165,7 +165,7 @@ let declare_one_prenex_implicit locality f =
| [] ->
errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| impls ->
- Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
+ Impargs.set_implicits locality fref [impls]
}
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 552a4048b1..fb99b87108 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a =
loop 0
let unif_HO env ise p c =
- try Evarconv.the_conv_x env p c ise
+ try Evarconv.unify_delay env ise p c
with Evarconv.UnableToUnify(ise, err) ->
raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:23:50 +0000