aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore3
-rw-r--r--dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh6
-rw-r--r--doc/sphinx/practical-tools/utilities.rst8
-rw-r--r--doc/sphinx/proof-engine/tactics.rst14
-rw-r--r--pretyping/evarconv.ml74
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/reductionops.ml5
-rw-r--r--pretyping/reductionops.mli3
-rw-r--r--pretyping/unification.ml8
-rw-r--r--test-suite/output/Error_msg_diffs.v2
-rw-r--r--test-suite/success/ROmega3.v35
-rw-r--r--vernac/himsg.ml1
12 files changed, 71 insertions, 90 deletions
diff --git a/.gitignore b/.gitignore
index 8fd9fc614c..5264968e95 100644
--- a/.gitignore
+++ b/.gitignore
@@ -165,7 +165,8 @@ ide/index_urls.txt
# coqide generated files (when testing)
*.crashcoqide
-user-contrib
+/user-contrib/*
+!/user-contrib/Ltac2
.*.sw*
.#*
diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
new file mode 100644
index 0000000000..0e1449f36c
--- /dev/null
+++ b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then
+
+ unicoq_CI_REF=whd-for-evar-conv-no-stack
+ unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 35231610fe..554f6bf230 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -909,13 +909,15 @@ Command line options
:--coqlib url: Set base URL for the Coq standard library (default is
`<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url
Coq``.
- :-R dir coqdir: Map physical directory dir to |Coq| logical
+ :-R dir coqdir: Recursively map physical directory dir to |Coq| logical
directory ``coqdir`` (similarly to |Coq| option ``-R``).
+ :-Q dir coqdir: Map physical directory dir to |Coq| logical
+ directory ``coqdir`` (similarly to |Coq| option ``-Q``).
.. note::
- option ``-R`` only has
- effect on the files *following* it on the command line, so you will
+ options ``-R`` and ``-Q`` only have
+ effect on the files *following* them on the command line, so you will
probably need to put this option first.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 658ac857fb..0f78a9b84a 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3863,9 +3863,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
terms and input heads *must not* contain existential variables or be
existential variables respectively, while outputs can be any term. Multiple
modes can be declared for a single identifier, in that case only one mode
- needs to match the arguments for the hints to be applied.The head of a term
+ needs to match the arguments for the hints to be applied. The head of a term
is understood here as the applicative head, or the match or projection
- scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
+ scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is
especially useful for typeclasses, when one does not want to support default
instances and avoid ambiguity in general. Setting a parameter of a class as an
input forces proof-search to be driven by that index of the class, with ``!``
@@ -3874,8 +3874,14 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
.. note::
- One can use an ``Extern`` hint with no pattern to do pattern matching on
- hypotheses using ``match goal with`` inside the tactic.
+ + One can use a :cmd:`Hint Extern` with no pattern to do
+ pattern matching on hypotheses using ``match goal with``
+ inside the tactic.
+
+ + If you want to add hints such as :cmd:`Hint Transparent`,
+ :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass
+ resolution, do not forget to put them in the
+ ``typeclass_instances`` hint database.
Hint databases defined in the Coq standard library
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0ccc4fd9f9..99013a19c9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -146,8 +146,8 @@ let flex_kind_of_term flags env evd c sk =
let apprec_nohdbeta flags env evd c =
let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
if flags.modulo_betaiota && Stack.not_purely_applicative sk
- then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env evd Cst_stack.empty appr))
+ then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state
+ flags.open_ts env evd appr)
else c
let position_problem l2r = function
@@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
let term2 = apprec_nohdbeta flags env evd term2 in
let default () =
evar_eqappr_x flags env evd pbty
- (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
- (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
+ (whd_nored_state evd (term1,Stack.empty))
+ (whd_nored_state evd (term2,Stack.empty))
in
begin match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
@@ -525,7 +525,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
end
and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
- ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
+ (term1, sk1 as appr1) (term2, sk2 as appr2) =
let quick_fail i = (* not costly, loses info *)
UnifFailure (i, NotSameHead)
in
@@ -555,8 +555,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
let c = nf_evar evd c1 in
let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env' evd Cst_stack.empty (c'1, Stack.empty) in
- let out2 = whd_nored_state evd
+ flags.open_ts env' evd (c'1, Stack.empty) in
+ let out2, _ = whd_nored_state evd
(lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
Cst_stack.empty in
if onleft then evar_eqappr_x flags env' evd CONV out1 out2
@@ -636,11 +636,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
else quick_fail i)
ev lF tM i
in
- let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
+ let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) vM =
let switch f a b = if on_left then f a b else f b a in
let delta i =
- switch (evar_eqappr_x flags env i pbty) (apprF,cstsF)
- (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i cstsM (vM,skM))
+ switch (evar_eqappr_x flags env i pbty) apprF
+ (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM))
in
let default i = ise_try i [miller on_left ev apprF apprM;
consume on_left apprF apprM;
@@ -658,11 +658,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
let f =
try
let termM' = Retyping.expand_projection env evd p c [] in
- let apprM', cstsM' =
- whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd cstsM (termM',skM)
+ let apprM' =
+ whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (termM',skM)
in
let delta' i =
- switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) (apprM',cstsM')
+ switch (evar_eqappr_x flags env i pbty) apprF apprM'
in
fun i -> ise_try i [miller on_left ev apprF apprM';
consume on_left apprF apprM'; delta']
@@ -718,7 +718,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
(position_problem true pbty,destEvar i' ev1',term2)
else
evar_eqappr_x flags env evd pbty
- ((ev1', sk1), csts1) ((term2, sk2), csts2)
+ (ev1', sk1) (term2, sk2)
| Some (r,[]), Success i' ->
(* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
(* we now unify r[?ev1] and ?ev2 *)
@@ -728,7 +728,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
(position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r))
else
evar_eqappr_x flags env evd pbty
- ((ev2', sk1), csts1) ((term2, sk2), csts2)
+ (ev2', sk1) (term2, sk2)
| Some ([],r), Success i' ->
(* Symmetrically *)
(* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
@@ -738,7 +738,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
solve_simple_eqn (conv_fun evar_conv_x) flags env i'
(position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r))
else evar_eqappr_x flags env evd pbty
- ((ev1', sk1), csts1) ((term2, sk2), csts2)
+ (ev1', sk1) (term2, sk2)
| None, (UnifFailure _ as x) ->
(* sk1 and sk2 have no common outer part *)
if Stack.not_purely_applicative sk2 then
@@ -808,10 +808,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
ise_try evd [f1; f2; f3; f4; f5]
| Flexible ev1, MaybeFlexible v2 ->
- flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2
+ flex_maybeflex true ev1 appr1 appr2 v2
| MaybeFlexible v1, Flexible ev2 ->
- flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1
+ flex_maybeflex false ev2 appr2 appr1 v1
| MaybeFlexible v1, MaybeFlexible v2 -> begin
match EConstr.kind evd term1, EConstr.kind evd term2 with
@@ -829,8 +829,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1)
+ and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2)
in evar_eqappr_x flags env i pbty out1 out2
in
ise_try evd [f1; f2]
@@ -841,8 +841,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
[(fun i -> evar_conv_x flags env i CONV c c');
(fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)]
and f2 i =
- let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1)
- and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2)
+ let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1)
+ and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2)
in evar_eqappr_x flags env i pbty out1 out2
in
ise_try evd [f1; f2]
@@ -855,8 +855,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
(match res with
| Some (f1,args1) ->
- evar_eqappr_x flags env evd pbty ((f1,Stack.append_app args1 sk1),csts1)
- (appr2,csts2)
+ evar_eqappr_x flags env evd pbty (f1,Stack.append_app args1 sk1)
+ appr2
| None -> UnifFailure (evd,NotSameHead))
| Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
@@ -866,7 +866,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
(match res with
| Some (f2,args2) ->
- evar_eqappr_x flags env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
+ evar_eqappr_x flags env evd pbty appr1 (f2,Stack.append_app args2 sk2)
| None -> UnifFailure (evd,NotSameHead))
| _, _ ->
@@ -906,16 +906,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
(* false (* immediate solution without Canon Struct *)*)
| Lambda _ -> assert (match args with [] -> true | _ -> false); true
| LetIn (_,b,_,c) -> is_unnamed
- (fst (whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i Cst_stack.empty (subst1 b c, args)))
+ (whd_betaiota_deltazeta_for_iota_state
+ flags.open_ts env i (subst1 b c, args))
| Fix _ -> true (* Partially applied fix can be the result of a whd call *)
| Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
| Case _ | App _| Cast _ -> assert false in
let rhs_is_stuck_and_unnamed () =
let applicative_stack = fst (Stack.strip_app sk2) in
is_unnamed
- (fst (whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i Cst_stack.empty (v2, applicative_stack))) in
+ (whd_betaiota_deltazeta_for_iota_state
+ flags.open_ts env i (v2, applicative_stack)) in
let rhs_is_already_stuck =
rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in
@@ -923,12 +923,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
&& (not (Stack.not_purely_applicative sk1)) then
evar_eqappr_x ~rhs_is_already_stuck flags env i pbty
(whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
- (appr2,csts2)
+ flags.open_ts env i(v1,sk1))
+ appr2
else
- evar_eqappr_x flags env i pbty (appr1,csts1)
+ evar_eqappr_x flags env i pbty appr1
(whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ flags.open_ts env i (v2,sk2))
in
ise_try evd [f1; f2; f3]
end
@@ -957,8 +957,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
and f4 i =
evar_eqappr_x flags env i pbty
(whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
- (appr2,csts2)
+ flags.open_ts env i (v1,sk1))
+ appr2
in
ise_try evd [f3; f4]
@@ -969,9 +969,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
else conv_record flags env i (check_conv_record env i appr2 appr1)
with Not_found -> UnifFailure (i,NoCanonicalStructure))
and f4 i =
- evar_eqappr_x flags env i pbty (appr1,csts1)
+ evar_eqappr_x flags env i pbty appr1
(whd_betaiota_deltazeta_for_iota_state
- flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
+ flags.open_ts env i (v2,sk2))
in
ise_try evd [f3; f4]
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 0fe47c2a48..bf83f5e88f 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -144,7 +144,7 @@ val evar_unify : Evarsolve.unifier
(* For debugging *)
val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags ->
env -> evar_map ->
- conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
+ conv_pb -> state -> state ->
Evarsolve.unification_result
val occur_rigidly : Evarsolve.unify_flags ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1871609e18..120b4e6f00 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1675,7 +1675,7 @@ let is_sort env sigma t =
(* reduction to head-normal-form allowing delta/zeta only in argument
of case/fix (heuristic used by evar_conv) *)
-let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+let whd_betaiota_deltazeta_for_iota_state ts env sigma s =
let refold = false in
let tactic_mode = false in
let rec whrec csts s =
@@ -1696,7 +1696,8 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'')
else s,csts'
|_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts'
- in whrec csts s
+ in
+ fst (whrec Cst_stack.empty s)
let find_conclusion env sigma =
let rec decrec env c =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5938d9b367..b5d3ff7627 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -312,8 +312,7 @@ val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
- TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
- state * Cst_stack.t
+ TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9ba51dcfa9..d134c7319f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -489,8 +489,8 @@ let unfold_projection env p stk =
let expand_key ts env sigma = function
| Some (IsKey k) -> Option.map EConstr.of_constr (expand_table_key env k)
| Some (IsProj (p, c)) ->
- let red = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
- Cst_stack.empty (c, unfold_projection env p [])))
+ let red = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma
+ (c, unfold_projection env p []))
in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red
| None -> None
@@ -597,8 +597,8 @@ let constr_cmp pb env sigma flags t u =
None
let do_reduce ts (env, nb) sigma c =
- Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
- ts env sigma Cst_stack.empty (c, Stack.empty)))
+ Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
+ ts env sigma (c, Stack.empty))
let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
| Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
diff --git a/test-suite/output/Error_msg_diffs.v b/test-suite/output/Error_msg_diffs.v
index 11c766b210..a26e683398 100644
--- a/test-suite/output/Error_msg_diffs.v
+++ b/test-suite/output/Error_msg_diffs.v
@@ -1,4 +1,4 @@
-(* coq-prog-args: ("-color" "on" "-async-proofs" "off") *)
+(* coq-prog-args: ("-color" "on" "-diffs" "on" "-async-proofs" "off") *)
(* Re: -async-proofs off, see https://github.com/coq/coq/issues/9671 *)
(* Shows diffs in an error message for an "Unable to unify" error *)
Require Import Arith List Bool.
diff --git a/test-suite/success/ROmega3.v b/test-suite/success/ROmega3.v
deleted file mode 100644
index ef9cb17b4b..0000000000
--- a/test-suite/success/ROmega3.v
+++ /dev/null
@@ -1,35 +0,0 @@
-
-Require Import ZArith Lia.
-Local Open Scope Z_scope.
-
-(** Benchmark provided by Chantal Keller, that romega used to
- solve far too slowly (compared to omega or lia). *)
-
-(* In Coq 8.9 (end of 2018), the `romega` tactics are deprecated.
- The tests in this file remain but now call the `lia` tactic. *)
-
-
-Parameter v4 : Z.
-Parameter v3 : Z.
-Parameter o4 : Z.
-Parameter s5 : Z.
-Parameter v2 : Z.
-Parameter o5 : Z.
-Parameter s6 : Z.
-Parameter v1 : Z.
-Parameter o6 : Z.
-Parameter s7 : Z.
-Parameter v0 : Z.
-Parameter o7 : Z.
-
-Lemma lemma_5833 :
- ~ 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
- (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
- (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 8192
-\/
- 16 * v4 + (8 * v3 + (-8192 * o4 + (-4096 * s5 + (4 * v2 +
- (-4096 * o5 + (-2048 * s6 + (2 * v1 + (-2048 * o6 +
- (-1024 * s7 + (v0 + -1024 * o7)))))))))) >= 1024.
-Proof.
-Timeout 1 lia. (* should take a few milliseconds, not seconds *)
-Timeout 1 Qed. (* ditto *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 082b22b373..f58eeae6dc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -150,6 +150,7 @@ let explicit_flags =
[print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
let with_diffs pm pn =
+ if not (Proof_diffs.show_diffs ()) then pm, pn else
try
let tokenize_string = Proof_diffs.tokenize_string in
Pp_diff.diff_pp ~tokenize_string pm pn
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 04:03:52 +0000