aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitattributes79
-rw-r--r--CHANGES3
-rw-r--r--plugins/ssrmatching/ssrmatching.ml48
-rw-r--r--pretyping/nativenorm.ml28
-rw-r--r--pretyping/unification.ml9
-rw-r--r--pretyping/unification.mli3
-rw-r--r--pretyping/vnorm.ml20
-rw-r--r--tactics/tactics.ml45
-rw-r--r--test-suite/Makefile15
-rw-r--r--test-suite/README.md14
-rw-r--r--test-suite/bugs/closed/7068.v6
-rw-r--r--test-suite/bugs/closed/7076.v4
12 files changed, 149 insertions, 85 deletions
diff --git a/.gitattributes b/.gitattributes
index e087e17379..a5edcdb5bf 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -5,48 +5,51 @@
# Because our commit hook automatically does [apply whitespace=fix] we
# disable whitespace checking for all files except those where we want
# it. Otherwise rogue global configuration and forgotten local
-# configuration can break commits.
+# configuration can break commits. Note that git cannot fix but can
+# detect a blank-at-eof when it comes from removing a chunk of text at
+# the end of the file, leaving an extra newline from before that
+# chunk, so we disable blank-at-eof.
* -whitespace
# tabs are allowed in Makefiles.
-Makefile* whitespace=trailing-space
-tools/CoqMakefile.in whitespace=trailing-space
+Makefile* whitespace=blank-at-eol
+tools/CoqMakefile.in whitespace=blank-at-eol
# in general we don't want tabs.
-*.asciidoc whitespace=trailing-space,tab-in-indent
-*.bib whitespace=trailing-space,tab-in-indent
-*.c whitespace=trailing-space,tab-in-indent
-*.css whitespace=trailing-space,tab-in-indent
-*.dtd whitespace=trailing-space,tab-in-indent
-*.el whitespace=trailing-space,tab-in-indent
-*.g whitespace=trailing-space,tab-in-indent
-*.h whitespace=trailing-space,tab-in-indent
-*.html whitespace=trailing-space,tab-in-indent
-*.hva whitespace=trailing-space,tab-in-indent
-*.js whitespace=trailing-space,tab-in-indent
-*.json whitespace=trailing-space,tab-in-indent
-*.lang whitespace=trailing-space,tab-in-indent
-*.md whitespace=trailing-space,tab-in-indent
-*.merlin whitespace=trailing-space,tab-in-indent
-*.ml whitespace=trailing-space,tab-in-indent
-*.ml4 whitespace=trailing-space,tab-in-indent
-*.mli whitespace=trailing-space,tab-in-indent
-*.mll whitespace=trailing-space,tab-in-indent
-*.mllib whitespace=trailing-space,tab-in-indent
-*.mlp whitespace=trailing-space,tab-in-indent
-*.mlpack whitespace=trailing-space,tab-in-indent
-*.nsh whitespace=trailing-space,tab-in-indent
-*.nsi whitespace=trailing-space,tab-in-indent
-*.py whitespace=trailing-space,tab-in-indent
-*.rst whitespace=trailing-space,tab-in-indent
-*.sh whitespace=trailing-space,tab-in-indent
-*.sty whitespace=trailing-space,tab-in-indent
-*.tex whitespace=trailing-space,tab-in-indent
-*.tokens whitespace=trailing-space,tab-in-indent
-*.txt whitespace=trailing-space,tab-in-indent
-*.v whitespace=trailing-space,tab-in-indent
-*.xml whitespace=trailing-space,tab-in-indent
-*.yml whitespace=trailing-space,tab-in-indent
+*.asciidoc whitespace=blank-at-eol,tab-in-indent
+*.bib whitespace=blank-at-eol,tab-in-indent
+*.c whitespace=blank-at-eol,tab-in-indent
+*.css whitespace=blank-at-eol,tab-in-indent
+*.dtd whitespace=blank-at-eol,tab-in-indent
+*.el whitespace=blank-at-eol,tab-in-indent
+*.g whitespace=blank-at-eol,tab-in-indent
+*.h whitespace=blank-at-eol,tab-in-indent
+*.html whitespace=blank-at-eol,tab-in-indent
+*.hva whitespace=blank-at-eol,tab-in-indent
+*.js whitespace=blank-at-eol,tab-in-indent
+*.json whitespace=blank-at-eol,tab-in-indent
+*.lang whitespace=blank-at-eol,tab-in-indent
+*.md whitespace=blank-at-eol,tab-in-indent
+*.merlin whitespace=blank-at-eol,tab-in-indent
+*.ml whitespace=blank-at-eol,tab-in-indent
+*.ml4 whitespace=blank-at-eol,tab-in-indent
+*.mli whitespace=blank-at-eol,tab-in-indent
+*.mll whitespace=blank-at-eol,tab-in-indent
+*.mllib whitespace=blank-at-eol,tab-in-indent
+*.mlp whitespace=blank-at-eol,tab-in-indent
+*.mlpack whitespace=blank-at-eol,tab-in-indent
+*.nsh whitespace=blank-at-eol,tab-in-indent
+*.nsi whitespace=blank-at-eol,tab-in-indent
+*.py whitespace=blank-at-eol,tab-in-indent
+*.rst whitespace=blank-at-eol,tab-in-indent
+*.sh whitespace=blank-at-eol,tab-in-indent
+*.sty whitespace=blank-at-eol,tab-in-indent
+*.tex whitespace=blank-at-eol,tab-in-indent
+*.tokens whitespace=blank-at-eol,tab-in-indent
+*.txt whitespace=blank-at-eol,tab-in-indent
+*.v whitespace=blank-at-eol,tab-in-indent
+*.xml whitespace=blank-at-eol,tab-in-indent
+*.yml whitespace=blank-at-eol,tab-in-indent
# CR is desired for these Windows files.
-*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent
+*.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent
diff --git a/CHANGES b/CHANGES
index e8718bbab7..787c9ba12a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -25,6 +25,9 @@ Tactics
- Deprecated the Implicit Tactic family of commands.
+- The `simple apply` tactic now respects the `Opaque` flag when called from
+ Ltac (`auto` still does not respect it).
+
Tools
- Coq_makefile lets one override or extend the following variables from
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 93c63d522a..b1c5e131ff 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -312,20 +312,22 @@ let unif_HO_args env ise0 pa i ca =
(* for HO evars, though hopefully Miller patterns can pick up some of *)
(* those cases, and HO matching will mop up the rest. *)
let flags_FO env =
+ let oracle = Environ.oracle env in
+ let ts = Conv_oracle.get_transp_state oracle in
let flags =
- { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags
+ { (Unification.default_no_delta_unify_flags ts).Unification.core_unify_flags
with
Unification.modulo_conv_on_closed_terms = None;
Unification.modulo_eta = true;
Unification.modulo_betaiota = true;
- Unification.modulo_delta_types = Conv_oracle.get_transp_state (Environ.oracle env)}
+ Unification.modulo_delta_types = ts }
in
{ Unification.core_unify_flags = flags;
Unification.merge_unify_flags = flags;
Unification.subterm_unify_flags = flags;
Unification.allow_K_in_toplevel_higher_order_unification = false;
Unification.resolve_evars =
- (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars
+ (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars
}
let unif_FO env ise p c =
Unification.w_unify env ise Reduction.CONV ~flags:(flags_FO env)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 7666ce0eb9..4b8e0e0964 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -312,10 +312,10 @@ and nf_atom_type env sigma atom =
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
let params,realargs = Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env
+ hnf_prod_applist_assum env nparamdecls
(Inductiveops.type_of_inductive env ind) (Array.to_list params) in
- let pT = whd_all env pT in
let dep, p = nf_predicate env sigma ind mip params p pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
@@ -372,20 +372,24 @@ and nf_atom_type env sigma atom =
and nf_predicate env sigma ind mip params v pT =
- match kind_of_value v, kind pT with
- | Vfun f, Prod _ ->
+ match kind (whd_allnolet env pT) with
+ | LetIn (name,b,t,pT) ->
+ let dep,body =
+ nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+ dep, mkLetIn (name,b,t,body)
+ | Prod (name,dom,codom) -> begin
+ match kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let name,dom,codom =
- try decompose_prod env pT with
- DestKO ->
- CErrors.anomaly
- (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
- in
let dep,body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
- | Vfun f, _ ->
+ | _ -> false, nf_type env sigma v
+ end
+ | _ ->
+ match kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
let name = Name (Id.of_string "c") in
@@ -395,7 +399,7 @@ and nf_predicate env sigma ind mip params v pT =
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_type env sigma v
+ | _ -> false, nf_type env sigma v
and nf_evar env sigma evk ty args =
let evi = try Evd.find sigma evk with Not_found -> assert false in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a8a4003dc5..5cf6e4b262 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -398,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
modulo_betaiota = false;
}
-let default_no_delta_unify_flags () =
- let flags = default_no_delta_core_unify_flags () in {
+let default_no_delta_unify_flags ts =
+ let flags = default_no_delta_core_unify_flags () in
+ let flags = { flags with
+ modulo_conv_on_closed_terms = Some ts;
+ modulo_delta_types = ts
+ } in
+ {
core_unify_flags = flags;
merge_unify_flags = flags;
subterm_unify_flags = flags;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 16ce5c93d0..e2e261ae7a 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Names
open Constr
open EConstr
open Environ
@@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags
val default_no_delta_core_unify_flags : unit -> core_unify_flags
val default_unify_flags : unit -> unify_flags
-val default_no_delta_unify_flags : unit -> unify_flags
+val default_no_delta_unify_flags : transparent_state -> unify_flags
val elim_flags : unit -> unify_flags
val elim_no_delta_flags : unit -> unify_flags
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index a1ba4a6a98..14c9f49b12 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
- let pT = whd_all env pT in
let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env sigma ind mib mip u params dep p in
@@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk =
nf_stk env sigma (mkProj(p',c)) ty stk
and nf_predicate env sigma ind mip params v pT =
- match whd_val v, kind pT with
- | Vfun f, Prod _ ->
+ match kind (whd_allnolet env pT) with
+ | LetIn (name,b,t,pT) ->
+ let dep,body =
+ nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+ dep, mkLetIn (name,b,t,body)
+ | Prod (name,dom,codom) -> begin
+ match whd_val v with
+ | Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
- let name,dom,codom = decompose_prod env pT in
let dep,body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
- | Vfun f, _ ->
+ | _ -> assert false
+ end
+ | _ ->
+ match whd_val v with
+ | Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
let name = Name (Id.of_string "c") in
@@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT =
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_val env sigma v crazy_type
+ | _ -> false, nf_val env sigma v crazy_type
and nf_args env sigma vargs ?from:(f=0) t =
let t = ref t in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d7888f6ca2..b571b347d3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1637,13 +1637,11 @@ let tclORELSEOPT t k =
Proofview.tclZERO ~info e
| Some tac -> tac)
-let general_apply with_delta with_destruct with_evars clear_flag
- {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
+let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
+ clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -1652,7 +1650,12 @@ let general_apply with_delta with_destruct with_evars clear_flag
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
-
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
let try_apply thm_ty nprod =
try
@@ -1718,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function
(general_apply b b e k cb)
(apply_with_bindings_gen b e cbl)
-let apply_with_delayed_bindings_gen b e l =
+let apply_with_delayed_bindings_gen b e l =
let one k {CAst.loc;v=f} =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (sigma, cb) = f env sigma in
Tacticals.New.tclWITHHOLES e
- (general_apply b b e k CAst.(make ?loc cb)) sigma
+ (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma
end
in
let rec aux = function
@@ -1800,14 +1803,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
in
aux (make_clenv_binding env sigma (d,thm) lbind)
-let apply_in_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
+let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
let open Context.Rel.Declaration in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
- let flags =
- if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
@@ -1815,6 +1816,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
+ let ts =
+ if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+ else full_transparent_state
+ in
+ let flags =
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
try
let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1834,14 +1841,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
aux [] with_destruct d
end
-let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
- id (clear_flag,{CAst.loc;v=f}) tac =
+let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+ with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
let (sigma, c) = f env sigma in
Tacticals.New.tclWITHHOLES with_evars
- (apply_in_once sidecond_first with_delta with_destruct with_evars
+ (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
naming id (clear_flag,CAst.(make ?loc c)) tac)
sigma
end
@@ -2531,11 +2538,11 @@ let assert_as first hd ipat t =
(* apply in as *)
-let general_apply_in sidecond_first with_delta with_destruct with_evars
- id lemmas ipat =
+let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+ with_destruct with_evars id lemmas ipat =
let tac (naming,lemma) tac id =
- apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
- naming id lemma tac in
+ apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+ with_destruct with_evars naming id lemma tac in
Proofview.Goal.enter begin fun gl ->
let destopt =
if with_evars then MoveLast (* evars would depend on the whole context *)
@@ -2566,7 +2573,7 @@ let apply_in simple with_evars id lemmas ipat =
general_apply_in false simple simple with_evars id lemmas ipat
let apply_delayed_in simple with_evars id lemmas ipat =
- general_apply_in false simple simple with_evars id lemmas ipat
+ general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
(*****************************)
(* Tactics abstracting terms *)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f41fb5b1e4..32e245e362 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
@echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
$(HIDE){ \
echo $(call log_intro,$<); \
- tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+ output=$*.out.real; \
$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
| grep -v "Welcome to Coq" \
| grep -v "\[Loading ML file" \
| grep -v "Skipping rcfile loading" \
| grep -v "^<W>" \
| sed 's/File "[^"]*"/File "stdin"/' \
- > $$tmpoutput; \
- diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \
+ > $$output; \
+ diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
if [ $$R = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
+ rm $$output; \
else \
echo $(log_failure); \
echo " $<...Error! (unexpected output)"; \
$(FAIL); \
fi; \
- rm $$tmpoutput; \
} > "$@"
+.PHONY: approve-output
+approve-output: output
+ $(HIDE)for f in output/*.out.real; do \
+ mv "$$f" "$${f%.real}"; \
+ echo "Updated $${f%.real}!"; \
+ done
+
# the expected output for the MExtraction test is
# /plugins/micromega/micromega.ml except with additional newline
output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/README.md b/test-suite/README.md
index 4572c98cfe..ef2e574ece 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file
There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them.
+
+## Fixing output tests
+
+When an output test `output/foo.v` fails, the output is stored in
+`output/foo.out.real`. Move that file to the reference file
+`output/foo.out` to update the test, approving the new output. Target
+`approve-output` will do this for all failing output tests
+automatically.
+
+Don't forget to check the updated `.out` files into git!
+
+Note that `output/MExtraction.out` is special: it is copied from
+`micromega/micromega.ml` in the plugin source directory. Automatic
+approval will incorrectly update the copy.
diff --git a/test-suite/bugs/closed/7068.v b/test-suite/bugs/closed/7068.v
new file mode 100644
index 0000000000..9fadb195bf
--- /dev/null
+++ b/test-suite/bugs/closed/7068.v
@@ -0,0 +1,6 @@
+(* These tests are only about a subset of #7068 *)
+(* The original issue is still open *)
+
+Inductive foo : let T := Type in T := .
+Definition bob1 := Eval vm_compute in foo_rect.
+Definition bob2 := Eval native_compute in foo_rect.
diff --git a/test-suite/bugs/closed/7076.v b/test-suite/bugs/closed/7076.v
new file mode 100644
index 0000000000..0abc88c282
--- /dev/null
+++ b/test-suite/bugs/closed/7076.v
@@ -0,0 +1,4 @@
+(* These calls were raising an anomaly at some time *)
+Inductive A : nat -> id (nat->Type) := .
+Eval vm_compute in fun x => match x in A y z return y = z with end.
+Eval native_compute in fun x => match x in A y z return y = z with end.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 17:51:50 +0000