aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/g_class.mlg8
-rw-r--r--pretyping/pretyping.ml8
-rw-r--r--test-suite/bugs/closed/bug_12970.v4
-rw-r--r--test-suite/success/Nsatz.v56
4 files changed, 41 insertions, 35 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 8d197e6056..a86045b0a4 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) natural_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
@@ -87,11 +87,13 @@ END
(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
- { typeclasses_eauto ~strategy:Bfs ~depth:d l }
+ { typeclasses_eauto ~depth:d ~strategy:Bfs l }
| [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
{ typeclasses_eauto ~depth:d l }
+ | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) ] -> {
+ typeclasses_eauto ~depth:d ~strategy:Bfs ~only_classes:true [Class_tactics.typeclasses_db] }
| [ "typeclasses" "eauto" int_or_var_opt(d) ] -> {
- typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] }
+ typeclasses_eauto ~depth:d ~only_classes:true [Class_tactics.typeclasses_db] }
END
TACTIC EXTEND head_of_constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8f52018a44..268ad2ae56 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -857,7 +857,7 @@ struct
typing the argument, so we replace it by an existential
variable *)
let sigma, c_hole = new_evar env sigma ~src:(loc,Evar_kinds.InternalHole) c1 in
- (sigma, make_judge c_hole c1), (c_hole, c, trace) :: bidiargs
+ (sigma, make_judge c_hole c1), (c_hole, c1, c, trace) :: bidiargs
else
let tycon = Some c1 in
pretype tycon env sigma c, bidiargs
@@ -886,12 +886,10 @@ struct
let sigma, resj, resj_before_bidi, bidiargs = apply_rec env sigma 0 fj fj candargs [] args in
let sigma, resj = refresh_template env sigma resj in
let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma resj tycon in
- let refine_arg n (sigma,t) (newarg,origarg,trace) =
+ let refine_arg n (sigma,t) (newarg,ty,origarg,trace) =
(* Refine an argument (originally `origarg`) represented by an evar
(`newarg`) to use typing information from the context *)
- (* Recover the expected type of the argument *)
- let ty = Retyping.get_type_of !!env sigma newarg in
- (* Type the argument using this expected type *)
+ (* Type the argument using the expected type *)
let sigma, j = pretype (Some ty) env sigma origarg in
(* Unify the (possibly refined) existential variable with the
(typechecked) original value *)
diff --git a/test-suite/bugs/closed/bug_12970.v b/test-suite/bugs/closed/bug_12970.v
new file mode 100644
index 0000000000..69ce7ec2c2
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12970.v
@@ -0,0 +1,4 @@
+Arguments existT _ & _ _.
+
+Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y =>
+ existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)).
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 998f3f7dd1..73e98ea920 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,6 +1,8 @@
Require Import TestSuite.admit.
(* compile en user 3m39.915s sur cachalot *)
Require Import Nsatz.
+Require List.
+Import List.ListNotations.
(* Example with a generic domain *)
@@ -294,7 +296,7 @@ Lemma minh: forall A B C D O E H I:point,
Proof. geo_begin.
idtac "minh".
Time nsatz with radicalmax :=1%N strategy:=1%Z
- parameters:=(X O::X B::X C::nil)
+ parameters:=[X O; X B; X C]
variables:= (@nil R).
(*Finished transaction in 13. secs (10.102464u,0.s)
*)
@@ -314,15 +316,15 @@ Proof.
geo_begin.
idtac "Pappus".
Time nsatz with radicalmax :=1%N strategy:=0%Z
- parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil)
- variables:= (X B
- :: X A1
- :: Y A1
- :: X B1
- :: Y B1
- :: X C
- :: Y C1
- :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil).
+ parameters:=[X B; X A1; Y A1; X B1; Y B1; X C; Y C1]
+ variables:= [X B;
+ X A1;
+ Y A1;
+ X B1;
+ Y B1;
+ X C;
+ Y C1;
+ X C1; Y P; X P; Y Q; X Q; Y S; X S].
(*Finished transaction in 8. secs (7.795815u,0.000999999999999s)
*)
Qed.
@@ -347,7 +349,7 @@ Proof.
geo_begin.
idtac "Simson".
Time nsatz with radicalmax :=1%N strategy:=0%Z
- parameters:=(X B::Y B::X C::Y C::Y D::nil)
+ parameters:=[X B; Y B; X C; Y C; Y D]
variables:= (@nil R). (* compute -[X Y]. *)
(*Finished transaction in 8. secs (7.550852u,0.s)
*)
@@ -432,20 +434,20 @@ Proof.
geo_begin.
idtac "Desargues".
Time
-let lv := rev (X A
- :: X B
- :: Y B
- :: X C
- :: Y C
- :: Y A1 :: X A1
- :: Y B1
- :: Y C1
- :: X T
- :: Y T
- :: X Q
- :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
+let lv := rev [X A;
+ X B;
+ Y B;
+ X C;
+ Y C;
+ Y A1; X A1;
+ Y B1;
+ Y C1;
+ X T;
+ Y T;
+ X Q;
+ Y Q; X P; Y P; X C1; X B1] in
nsatz with radicalmax :=1%N strategy:=0%Z
- parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil)
+ parameters:=[X A; X B; Y B; X C; Y C; X A1; Y B1; Y C1]
variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*)
Qed.
@@ -522,9 +524,9 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
geo_begin.
idtac "hauteurs".
Time
- let lv := constr:(Y A1
- :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C
- :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+ let lv := constr:([Y A1;
+ X A1; Y B1; X B1; Y A; Y B; X B; X A; X H; Y C;
+ Y C1; Y H; X C1; X C]) in
nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R)
variables := lv.
(*Finished transaction in 5. secs (4.360337u,0.008999s)*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:16:33 +0000