aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/CODEOWNERS3
-rw-r--r--CHANGES.md7
-rw-r--r--Makefile.doc6
-rw-r--r--dev/doc/critical-bugs16
-rw-r--r--dev/nixpkgs.nix4
-rwxr-xr-xdev/tools/backport-pr.sh30
-rw-r--r--doc/sphinx/addendum/implicit-coercions.rst17
-rw-r--r--doc/sphinx/addendum/type-classes.rst2
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst4
-rw-r--r--ide/coqOps.ml2
-rw-r--r--ide/wg_Segment.ml83
-rw-r--r--ide/wg_Segment.mli2
-rw-r--r--plugins/ssr/ssrelim.ml64
-rw-r--r--plugins/ssr/ssrequality.ml17
-rw-r--r--plugins/ssr/ssripats.ml20
-rw-r--r--pretyping/classops.ml33
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/evarconv.ml17
-rw-r--r--stm/stm.ml5
-rw-r--r--test-suite/bugs/closed/bug_4157.v272
-rw-r--r--test-suite/bugs/closed/bug_9663.v2
-rw-r--r--test-suite/ssr/elim_noquant.v29
-rw-r--r--vernac/classes.ml2
24 files changed, 469 insertions, 178 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index f802040a1d..06a733be45 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -240,8 +240,7 @@ azure-pipelines.yml @coq/ci-maintainers
/theories/QArith/ @herbelin
-/theories/Reals/ @silene
-# Secondary maintainer @ppedrot
+/theories/Reals/ @coq/reals-library-maintainers
/theories/Relations/ @mattam82
# Secondary maintainer @ppedrot
diff --git a/CHANGES.md b/CHANGES.md
index 4a66fa423e..d43dc668e8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -149,6 +149,13 @@ Vernacular commands
- `Hypotheses` and `Variables` can now take implicit binders inside sections.
+- Removed deprecated option `Automatic Coercions Import`.
+
+- The `Show Script` command has been deprecated.
+
+- Option `Refine Instance Mode` has been deprecated and will be removed in
+ the next version.
+
Tools
- The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/Makefile.doc b/Makefile.doc
index 5ac3ecb63d..e89a20393c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -31,7 +31,13 @@ DVIPS:=dvips
HTMLSTYLE:=coqremote
# Sphinx-related variables
+OSNAME:=$(shell uname -o)
+ifeq ($(OSNAME),Cygwin)
+WIN_CURDIR:=$(shell cygpath -w $(CURDIR))
+SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)"
+else
SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)"
+endif
SPHINXOPTS= -j4
SPHINXWARNERROR ?= 1
ifeq ($(SPHINXWARNERROR),1)
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 8d78559c0d..c0a5b9095c 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -63,8 +63,8 @@ Typing constructions
impacted coqchk versions: ?
fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
found by: Georgi Guninski
- exploit: test-suite/bugs/closed/4294.v
- GH issue number: #4294
+ exploit: test-suite/failure/prop_set_proof_irrelevance.v
+ GH issue number: none?
risk: ?
Module system
@@ -77,7 +77,7 @@ Module system
impacted coqchk versions: ?
fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
found by: Dénès
- exploit: test-suite/bugs/closed/4294.v
+ exploit: test-suite/bugs/closed/bug_4294.v
GH issue number: #4294
risk: ?
@@ -105,7 +105,7 @@ Universes
impacted coqchk versions: ?
fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin),
found by: Barras
- exploit: test-suite/failure/inductive4.v
+ exploit: test-suite/failure/inductive.v
GH issue number: none
risk: unlikely to be activated by chance
@@ -141,7 +141,7 @@ Primitive projections
impacted coqchk versions: ?
fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
found by: Dénès exploiting bug #4588
- exploit: test-suite/bugs/closed/4588.v
+ exploit: test-suite/bugs/closed/bug_4588.v
GH issue number: #4588
risk: ?
@@ -167,7 +167,7 @@ Conversion machines
impacted coqchk versions: none (no virtual machine in coqchk)
fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
found by: Dénès, Pédrot
- exploit: test-suite/failure/vm-bug4157.v
+ exploit: test-suite/bugs/closed/bug_4157.v
GH issue number: #4157
risk:
@@ -179,7 +179,7 @@ Conversion machines
impacted coqchk versions: none (no virtual machine in coqchk)
fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
found by: Dénès
- exploit: test-suite/bugs/closed/6677.v
+ exploit: test-suite/bugs/closed/bug_6677.v
GH issue number: #6677
risk:
@@ -203,7 +203,7 @@ Conversion machines
impacted coqchk versions: none (no native computation in coqchk)
fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey),
found by: Letouzey, Dénès
- exploit: lost?
+ exploit: see commit message for 244d7a9aa
GH issue number: ?
risk:
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index 4aa0f04964..f4786d9431 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
import (fetchTarball {
- url = "https://github.com/NixOS/nixpkgs/archive/2923bd5d0669f1ec6ab03ddce052e9c5efb46d8f.tar.gz";
- sha256 = "16cn93rpxfql5idhigyjyhc013a3hwzyy2dl1xv7h2p78sk728vw";
+ url = "https://github.com/NixOS/nixpkgs/archive/8471ab76242987b11afd4486b82888e1588f8307.tar.gz";
+ sha256 = "06pp6b6x78jlinxifnphkbp79dx58jr990fkm4qziq0ay5klpxd7";
})
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index 9864fd4d69..1ec8251f66 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -30,13 +30,15 @@ while [[ $# -gt 0 ]]; do
esac
done
-if ! git log master --grep "Merge PR #${PRNUM}" | grep "." > /dev/null; then
+MASTER=origin/master
+
+if ! git log $MASTER --grep "Merge PR #$PRNUM" | grep "." > /dev/null; then
echo "PR #${PRNUM} does not exist."
exit 1
fi
-SIGNATURE_STATUS=$(git log master --grep "Merge PR #${PRNUM}" --format="%G?")
-git log master --grep "Merge PR #${PRNUM}" --format="%GG"
+SIGNATURE_STATUS=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%G?")
+git log $MASTER --grep "Merge PR #$PRNUM" --format="%GG"
if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
echo
read -p "Merge commit does not have a good (valid) signature. Bypass? [y/N] " -n 1 -r
@@ -47,10 +49,18 @@ if [[ "$NO_SIGNATURE_CHECK" != "true" && "$SIGNATURE_STATUS" != "G" ]]; then
fi
BRANCH=backport-pr-${PRNUM}
-RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
-MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
+RANGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%P" | sed 's/ /../')
+MESSAGE=$(git log $MASTER --grep "Merge PR #$PRNUM" --format="%s" | sed 's/Merge/Backport/')
-if git checkout -b "${BRANCH}"; then
+if [[ "$(git rev-parse --abbrev-ref HEAD)" == "$BRANCH" ]]; then
+
+ if ! git cherry-pick --continue; then
+ echo "Please fix the conflicts, then relaunch the script."
+ exit 1
+ fi
+ git checkout -
+
+elif git checkout -b "$BRANCH"; then
if ! git cherry-pick -x "${RANGE}"; then
if [[ "$NO_CONFLICTS" == "true" ]]; then
@@ -61,12 +71,8 @@ if git checkout -b "${BRANCH}"; then
git branch -d "$BRANCH"
exit 1
fi
- echo "Please fix the conflicts, then exit."
- bash
- while ! git cherry-pick --continue; do
- echo "Please fix the conflicts, then exit."
- bash
- done
+ echo "Please fix the conflicts, then relaunch the script."
+ exit 1
fi
git checkout -
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index d15aacad44..795fccbf08 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -322,21 +322,8 @@ are also forgotten.
Coercions and Modules
---------------------
-.. flag:: Automatic Coercions Import
-
- Since |Coq| version 8.3, the coercions present in a module are activated
- only when the module is explicitly imported. Formerly, the coercions
- were activated as soon as the module was required, whether it was
- imported or not.
-
- This option makes it possible to recover the behavior of the versions of
- |Coq| prior to 8.3.
-
-.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it.
-
- This warning is emitted when typechecking relies on a coercion
- contained in a module that has not been explicitely imported. It helps
- migrating code and stop relying on the option above.
+The coercions present in a module are activated only when the module is
+explicitly imported.
Examples
--------
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 3f5035d4a4..b069cf27f4 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -561,6 +561,8 @@ Settings
.. flag:: Refine Instance Mode
+ .. deprecated:: 8.10
+
This flag allows to switch the behavior of instance declarations made through
the Instance command.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 07215a0c7e..16b158c397 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -544,6 +544,10 @@ Requesting information
``<Your Tactic Text here>``.
+ .. deprecated:: 8.10
+
+ Please use a text editor.
+
.. cmdv:: Show Proof
:name: Show Proof
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 4aa801c2b2..8da9900724 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -250,7 +250,6 @@ object(self)
feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
let md = segment_model document in
segment#set_model md;
-(*
let on_click id =
let find _ _ s = Int.equal s.index id in
let sentence = Doc.find document find in
@@ -267,7 +266,6 @@ object(self)
ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
in
let _ = segment#connect#clicked ~callback:on_click in
-*)
()
method private tooltip_callback ~x ~y ~kbd tooltip =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 2e5de64254..b62c0a2190 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -8,10 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(*
open Util
open Preferences
-*)
type color = GDraw.color
@@ -24,7 +22,6 @@ object
method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
end
-(*
let i2f = float_of_int
let f2i = int_of_float
@@ -35,14 +32,20 @@ let color_eq (c1 : GDraw.color) (c2 : GDraw.color) = match c1, c2 with
| `RGB (r1, g1, b1), `RGB (r2, g2, b2) -> r1 = r2 && g1 = g2 && b1 = b2
| `WHITE, `WHITE -> true
| _ -> false
-*)
+
+let set_cairo_color ctx c =
+ let open Gdk.Color in
+ let c = GDraw.color c in
+ let cast i = i2f i /. 65536. in
+ Cairo.set_source_rgb ctx (cast @@ red c) (cast @@ green c) (cast @@ blue c)
+
class type segment_signals =
object
inherit GObj.misc_signals
inherit GUtil.add_ml_signals
method clicked : callback:(int -> unit) -> GtkSignal.id
end
-(*
+
class segment_signals_impl obj (clicked : 'a GUtil.signal) : segment_signals =
object
val after = false
@@ -50,14 +53,11 @@ object
inherit GUtil.add_ml_signals obj [clicked#disconnect]
method clicked = clicked#connect ~after
end
-*)
class segment () =
let box = GBin.frame () in
-(*
-let eventbox = GBin.event_box ~packing:box#add () in
-let draw = GMisc.image ~packing:eventbox#add () in
-*)
+let draw = GMisc.drawing_area ~packing:box#add () in
+
object (self)
inherit GObj.widget box#as_widget
@@ -66,56 +66,40 @@ object (self)
val mutable height = 20
val mutable model : model option = None
val mutable default : color = `WHITE
-(*
- val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
-*)
val clicked = new GUtil.signal ()
- val mutable need_refresh = false
- val refresh_timer = Ideutils.mktimer ()
-(*
+
initializer
box#misc#set_size_request ~height ();
let cb rect =
let w = rect.Gtk.width in
let h = rect.Gtk.height in
- (* Only refresh when size actually changed, otherwise loops *)
- if self#misc#visible && (width <> w || height <> h) then begin
- width <- w;
- height <- h;
- self#redraw ();
- end
+ width <- w;
+ height <- h
in
let _ = box#misc#connect#size_allocate ~callback:cb in
+ let () = draw#event#add [`BUTTON_PRESS] in
let clicked_cb ev = match model with
| None -> true
| Some md ->
let x = GdkEvent.Button.x ev in
- let (width, _) = pixmap#size in
let len = md#length in
let idx = f2i ((x *. i2f len) /. i2f width) in
let () = clicked#call idx in
true
in
- let _ = eventbox#event#connect#button_press ~callback:clicked_cb in
+ let _ = draw#event#connect#button_press ~callback:clicked_cb in
let cb show = if show then self#misc#show () else self#misc#hide () in
stick show_progress_bar self cb;
- (* Initial pixmap *)
- draw#set_pixmap pixmap;
- refresh_timer.Ideutils.run ~ms:300
- ~callback:(fun () -> if need_refresh then self#refresh (); true)
-*)
+ let cb ctx = self#refresh ctx; false in
+ let _ = draw#misc#connect#draw ~callback:cb in
+ ()
+
method set_model md =
model <- Some md;
- let changed_cb = function
- | `INSERT | `REMOVE ->
- if self#misc#visible then need_refresh <- true
- | `SET (i, color) ->
- ()
-(* if self#misc#visible then self#fill_range color i (i + 1)*)
- in
+ let changed_cb _ = self#misc#queue_draw () in
md#changed ~callback:changed_cb
-(*
- method private fill_range color i j = match model with
+
+ method private fill_range ctx color i j = match model with
| None -> ()
| Some md ->
let i = i2f i in
@@ -125,24 +109,19 @@ object (self)
let x = f2i ((i *. width) /. len) in
let x' = f2i ((j *. width) /. len) in
let w = x' - x in
- pixmap#set_foreground color;
- pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true ();
- draw#set_mask None;
+ set_cairo_color ctx color;
+ Cairo.rectangle ctx (i2f x) 0. ~w:(i2f w) ~h:(i2f height);
+ Cairo.fill ctx
method set_default_color color = default <- color
method default_color = default
- method private redraw () =
- pixmap <- GDraw.pixmap ~width ~height ();
- draw#set_pixmap pixmap;
- self#refresh ();
-
- method private refresh () = match model with
+ method private refresh ctx = match model with
| None -> ()
| Some md ->
- need_refresh <- false;
- pixmap#set_foreground default;
- pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
+ set_cairo_color ctx default;
+ Cairo.rectangle ctx 0. 0. ~w:(i2f width) ~h:(i2f height);
+ Cairo.fill ctx;
let make (k, cur, accu) v = match cur with
| None -> pred k, Some (k, k, v), accu
| Some (i, j, w) ->
@@ -154,11 +133,9 @@ object (self)
| None -> segments
| Some p -> p :: segments
in
- List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments;
- draw#set_mask None;
+ List.iter (fun (i, j, v) -> self#fill_range ctx v i (j + 1)) segments
method connect =
new segment_signals_impl box#as_widget clicked
-*)
end
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 84d487f35f..07f545fee7 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -31,9 +31,7 @@ class segment : unit ->
inherit GObj.widget
val obj : Gtk.widget Gtk.obj
method set_model : model -> unit
-(*
method connect : segment_signals
method default_color : color
method set_default_color : color -> unit
-*)
end
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 3fc05437da..94f7d24242 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -255,31 +255,49 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
(* Here we try to understand if the main pattern/term the user gave is
* the first pattern to be matched (i.e. if elimty ends in P t1 .. tn,
* weather tn is the t the user wrote in 'elim: t' *)
- let c_is_head_p, gl = match cty with
+ let c_is_head_p, gl =
+ match cty with
| None -> true, gl (* The user wrote elim: _ *)
| Some (c, c_ty, _) ->
- let res =
- (* we try to see if c unifies with the last arg of elim *)
- if elim_is_dep then None else
- let arg = List.assoc (n_elim_args - 1) elim_args in
- let gl, arg_ty = pfe_type_of gl arg in
- match saturate_until gl c c_ty (fun c c_ty gl ->
- pf_unify_HO (pf_unify_HO gl c_ty arg_ty) arg c) with
- | Some (c, _, _, gl) -> Some (false, gl)
- | None -> None in
- match res with
- | Some x -> x
- | None ->
- (* we try to see if c unifies with the last inferred pattern *)
- let inf_arg = List.hd inf_deps_r in
- let gl, inf_arg_ty = pfe_type_of gl inf_arg in
- match saturate_until gl c c_ty (fun _ c_ty gl ->
- pf_unify_HO gl c_ty inf_arg_ty) with
- | Some (c, _, _,gl) -> true, gl
- | None ->
- errorstrm Pp.(str"Unable to apply the eliminator to the term"++
- spc()++pr_econstr_env env (project gl) c++spc()++str"or to unify it's type with"++
- pr_econstr_env env (project gl) inf_arg_ty) in
+ let rec first = function
+ | [] ->
+ errorstrm Pp.(str"Unable to apply the eliminator to the term"++
+ spc()++pr_econstr_env env (project gl) c++spc())
+ | x :: rest ->
+ match x () with
+ | None -> first rest
+ | Some (b,gl) -> b, gl
+ in
+ (* Unify two terms if their heads are not applied unif variables, eg
+ * not (?P x). The idea is to rule out cases where the problem is too
+ * vague to drive the current heuristics. *)
+ let pf_unify_HO_rigid gl a b =
+ let is_applied_evar x = match EConstr.kind (project gl) x with
+ | App(x,_) -> EConstr.isEvar (project gl) x
+ | _ -> false in
+ if is_applied_evar a || is_applied_evar b then
+ raise Evarconv.(UnableToUnify(project gl,
+ Pretype_errors.ProblemBeyondCapabilities))
+ else pf_unify_HO gl a b in
+ let try_c_last_arg () =
+ (* we try to see if c unifies with the last arg of elim *)
+ if elim_is_dep then None else
+ let arg = List.assoc (n_elim_args - 1) elim_args in
+ let gl, arg_ty = pfe_type_of gl arg in
+ match saturate_until gl c c_ty (fun c c_ty gl ->
+ pf_unify_HO (pf_unify_HO_rigid gl c_ty arg_ty) arg c) with
+ | Some (c, _, _, gl) -> Some (false, gl)
+ | None -> None in
+ let try_c_last_pattern () =
+ (* we try to see if c unifies with the last inferred pattern *)
+ if inf_deps_r = [] then None else
+ let inf_arg = List.hd inf_deps_r in
+ let gl, inf_arg_ty = pfe_type_of gl inf_arg in
+ match saturate_until gl c c_ty (fun _ c_ty gl ->
+ pf_unify_HO_rigid gl c_ty inf_arg_ty) with
+ | Some (c, _, _,gl) -> Some(true, gl)
+ | None -> None in
+ first [try_c_last_arg;try_c_last_pattern] in
ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p));
let gl, predty = pfe_type_of gl pred in
(* Patterns for the inductive types indexes to be bound in pred are computed
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 15480c7a45..902098c8ce 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -325,7 +325,7 @@ let rec strip_prod_assum c = match Constr.kind c with
let rule_id = mk_internal_id "rewrite rule"
-exception PRtype_error
+exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
(* ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
@@ -351,7 +351,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
(* We check the proof is well typed *)
let sigma, proof_ty =
- try Typing.type_of env sigma proof with _ -> raise PRtype_error in
+ try Typing.type_of env sigma proof with
+ | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
+ | e when CErrors.noncritical e -> raise (PRtype_error None)
+ in
ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
try refine_with
~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
@@ -423,13 +426,17 @@ let rwcltac cl rdx dir sr gl =
in
let cvtac' _ =
try cvtac gl with
- | PRtype_error ->
+ | PRtype_error e ->
+ let error = Option.cata (fun (env, sigma, te) ->
+ Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
+ (Pp.mt ()) e in
if occur_existential (project gl) (Tacmach.pf_concl gl)
- then errorstrm Pp.(str "Rewriting impacts evars")
+ then errorstrm Pp.(str "Rewriting impacts evars" ++ error)
else errorstrm Pp.(str "Dependent type error in rewrite of "
++ pr_constr_env (pf_env gl) (project gl)
(Term.mkNamedLambda (make_annot pattern_id Sorts.Relevant)
- (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl)))
+ (EConstr.Unsafe.to_constr rdxt) (EConstr.Unsafe.to_constr cl))
+ ++ error)
in
tclTHEN cvtac' rwtac gl
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index e9fe1f3e48..3481b25c8b 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -369,18 +369,20 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl ->
end end
(*** [=> [: id]] ************************************************************)
-[@@@ocaml.warning "-3"]
let mk_abstract_id =
let open Coqlib in
let ssr_abstract_id = Summary.ref ~name:"SSR:abstractid" 0 in
-begin fun () ->
+begin fun env sigma ->
+ let sigma, zero = EConstr.fresh_global env sigma (lib_ref "num.nat.O") in
+ let sigma, succ = EConstr.fresh_global env sigma (lib_ref "num.nat.S") in
let rec nat_of_n n =
- if n = 0 then EConstr.mkConstruct path_of_O
- else EConstr.mkApp (EConstr.mkConstruct path_of_S, [|nat_of_n (n-1)|]) in
- incr ssr_abstract_id; nat_of_n !ssr_abstract_id
+ if n = 0 then zero
+ else EConstr.mkApp (succ, [|nat_of_n (n-1)|]) in
+ incr ssr_abstract_id;
+ sigma, nat_of_n !ssr_abstract_id
end
-let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
+let tclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
let env, concl = Goal.(env gl, concl gl) in
let step = begin fun sigma ->
let (sigma, (abstract_proof, abstract_ty)) =
@@ -389,8 +391,8 @@ let tcltclMK_ABSTRACT_VAR id = Goal.enter begin fun gl ->
let (sigma, ablock) = Ssrcommon.mkSsrConst "abstract_lock" env sigma in
let (sigma, lock) = Evarutil.new_evar env sigma ablock in
let (sigma, abstract) = Ssrcommon.mkSsrConst "abstract" env sigma in
- let abstract_ty =
- EConstr.mkApp(abstract, [|ty;mk_abstract_id ();lock|]) in
+ let (sigma, abstract_id) = mk_abstract_id env sigma in
+ let abstract_ty = EConstr.mkApp(abstract, [|ty; abstract_id; lock|]) in
let sigma, m = Evarutil.new_evar env sigma abstract_ty in
sigma, (m, abstract_ty) in
let sigma, kont =
@@ -409,7 +411,7 @@ end
let tclMK_ABSTRACT_VARS ids =
List.fold_right (fun id tac ->
- Tacticals.New.tclTHENFIRST (tcltclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
+ Tacticals.New.tclTHENFIRST (tclMK_ABSTRACT_VAR id) tac) ids (tclUNIT ())
(* Debugging *)
let tclLOG p t =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 54a1aa9aa0..ef918a614e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -120,9 +120,6 @@ let class_tab =
let coercion_tab =
Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
-let coercions_in_scope =
- Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty
-
module ClPairOrd =
struct
type t = cl_index * cl_index
@@ -400,13 +397,6 @@ let class_params = function
let add_class cl =
add_new_class cl { cl_param = class_params cl }
-let get_automatically_import_coercions =
- Goptions.declare_bool_option_and_ref
- ~depr:true (* Remove in 8.8 *)
- ~name:"automatic import of coercions"
- ~key:["Automatic";"Coercions";"Import"]
- ~value:false
-
let cache_coercion (_, c) =
let () = add_class c.coercion_source in
let () = add_class c.coercion_target in
@@ -422,20 +412,9 @@ let cache_coercion (_, c) =
let () = add_new_coercion c.coercion_type xf in
add_coercion_in_graph (xf,is,it)
-let load_coercion _ o =
- if get_automatically_import_coercions () then
- cache_coercion o
-
-let set_coercion_in_scope (_, c) =
- let r = c.coercion_type in
- coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
-
let open_coercion i o =
- if Int.equal i 1 then begin
- set_coercion_in_scope o;
- if not (get_automatically_import_coercions ()) then
- cache_coercion o
- end
+ if Int.equal i 1 then
+ cache_coercion o
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -469,10 +448,7 @@ let classify_coercion obj =
let inCoercion : coercion -> obj =
declare_object {(default_object "COERCION") with
open_function = open_coercion;
- load_function = load_coercion;
- cache_function = (fun objn ->
- set_coercion_in_scope objn;
- cache_coercion objn);
+ cache_function = cache_coercion;
subst_function = subst_coercion;
classify_function = classify_coercion;
discharge_function = discharge_coercion }
@@ -532,6 +508,3 @@ let hide_coercion coe =
let coe_info = coercion_info coe in
Some coe_info.coe_param
else None
-
-let is_coercion_in_scope r =
- GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 7c4842c8ae..ed2c5478f0 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -113,5 +113,3 @@ val coercions : unit -> coe_info_typ list
(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option
-
-val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 82411ba2ef..8c9b6550f3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -368,20 +368,12 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
-let warn_coercion_not_in_scope =
- CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
- Pp.(fun r -> str "Coercion used but not in scope: " ++
- Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
- ++ str "this coercion, please Import the module that contains it.")
-
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
- if not (is_coercion_in_scope i.coe_value) then
- warn_coercion_not_in_scope i.coe_value;
let isid = i.coe_is_identity in
let isproj = i.coe_is_projection in
let sigma, c = new_global sigma i.coe_value in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28a97bb91a..0ccc4fd9f9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -503,14 +503,23 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
| Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem true pbty,ev,term2) with
- | UnifFailure (_,OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
+ (* Eta-expansion might apply *)
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem false pbty,ev,term1) with
- | UnifFailure (_, OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _ -> default ()
end
diff --git a/stm/stm.ml b/stm/stm.ml
index ab388977a5..0c5d0c7b5d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1121,7 +1121,12 @@ let get_script prf =
in
find [] (VCS.get_branch_pos branch)
+let warn_show_script_deprecated =
+ CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated"
+ (fun () -> Pp.str "The “Show Script” command is deprecated.")
+
let show_script ?proof () =
+ warn_show_script_deprecated ();
try
let prf =
try match proof with
diff --git a/test-suite/bugs/closed/bug_4157.v b/test-suite/bugs/closed/bug_4157.v
new file mode 100644
index 0000000000..a9e96fcdde
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4157.v
@@ -0,0 +1,272 @@
+(** The following proof is due to a bug in `vm_compute` and was found by
+ Maxime Dénès and Pierre-Marie Pédrot. *)
+Inductive t :=
+| C_0 : nat -> t
+| C_1 : nat -> t
+| C_2 : nat -> t
+| C_3 : nat -> t
+| C_4 : nat -> t
+| C_5 : nat -> t
+| C_6 : nat -> t
+| C_7 : nat -> t
+| C_8 : nat -> t
+| C_9 : nat -> t
+| C_10 : nat -> t
+| C_11 : nat -> t
+| C_12 : nat -> t
+| C_13 : nat -> t
+| C_14 : nat -> t
+| C_15 : nat -> t
+| C_16 : nat -> t
+| C_17 : nat -> t
+| C_18 : nat -> t
+| C_19 : nat -> t
+| C_20 : nat -> t
+| C_21 : nat -> t
+| C_22 : nat -> t
+| C_23 : nat -> t
+| C_24 : nat -> t
+| C_25 : nat -> t
+| C_26 : nat -> t
+| C_27 : nat -> t
+| C_28 : nat -> t
+| C_29 : nat -> t
+| C_30 : nat -> t
+| C_31 : nat -> t
+| C_32 : nat -> t
+| C_33 : nat -> t
+| C_34 : nat -> t
+| C_35 : nat -> t
+| C_36 : nat -> t
+| C_37 : nat -> t
+| C_38 : nat -> t
+| C_39 : nat -> t
+| C_40 : nat -> t
+| C_41 : nat -> t
+| C_42 : nat -> t
+| C_43 : nat -> t
+| C_44 : nat -> t
+| C_45 : nat -> t
+| C_46 : nat -> t
+| C_47 : nat -> t
+| C_48 : nat -> t
+| C_49 : nat -> t
+| C_50 : nat -> t
+| C_51 : nat -> t
+| C_52 : nat -> t
+| C_53 : nat -> t
+| C_54 : nat -> t
+| C_55 : nat -> t
+| C_56 : nat -> t
+| C_57 : nat -> t
+| C_58 : nat -> t
+| C_59 : nat -> t
+| C_60 : nat -> t
+| C_61 : nat -> t
+| C_62 : nat -> t
+| C_63 : nat -> t
+| C_64 : nat -> t
+| C_65 : nat -> t
+| C_66 : nat -> t
+| C_67 : nat -> t
+| C_68 : nat -> t
+| C_69 : nat -> t
+| C_70 : nat -> t
+| C_71 : nat -> t
+| C_72 : nat -> t
+| C_73 : nat -> t
+| C_74 : nat -> t
+| C_75 : nat -> t
+| C_76 : nat -> t
+| C_77 : nat -> t
+| C_78 : nat -> t
+| C_79 : nat -> t
+| C_80 : nat -> t
+| C_81 : nat -> t
+| C_82 : nat -> t
+| C_83 : nat -> t
+| C_84 : nat -> t
+| C_85 : nat -> t
+| C_86 : nat -> t
+| C_87 : nat -> t
+| C_88 : nat -> t
+| C_89 : nat -> t
+| C_90 : nat -> t
+| C_91 : nat -> t
+| C_92 : nat -> t
+| C_93 : nat -> t
+| C_94 : nat -> t
+| C_95 : nat -> t
+| C_96 : nat -> t
+| C_97 : nat -> t
+| C_98 : nat -> t
+| C_99 : nat -> t
+| C_100 : nat -> t
+| C_101 : nat -> t
+| C_102 : nat -> t
+| C_103 : nat -> t
+| C_104 : nat -> t
+| C_105 : nat -> t
+| C_106 : nat -> t
+| C_107 : nat -> t
+| C_108 : nat -> t
+| C_109 : nat -> t
+| C_110 : nat -> t
+| C_111 : nat -> t
+| C_112 : nat -> t
+| C_113 : nat -> t
+| C_114 : nat -> t
+| C_115 : nat -> t
+| C_116 : nat -> t
+| C_117 : nat -> t
+| C_118 : nat -> t
+| C_119 : nat -> t
+| C_120 : nat -> t
+| C_121 : nat -> t
+| C_122 : nat -> t
+| C_123 : nat -> t
+| C_124 : nat -> t
+| C_125 : nat -> t
+| C_126 : nat -> t
+| C_127 : nat -> t
+| C_128 : nat -> t
+| C_129 : nat -> t
+| C_130 : nat -> t
+| C_131 : nat -> t
+| C_132 : nat -> t
+| C_133 : nat -> t
+| C_134 : nat -> t
+| C_135 : nat -> t
+| C_136 : nat -> t
+| C_137 : nat -> t
+| C_138 : nat -> t
+| C_139 : nat -> t
+| C_140 : nat -> t
+| C_141 : nat -> t
+| C_142 : nat -> t
+| C_143 : nat -> t
+| C_144 : nat -> t
+| C_145 : nat -> t
+| C_146 : nat -> t
+| C_147 : nat -> t
+| C_148 : nat -> t
+| C_149 : nat -> t
+| C_150 : nat -> t
+| C_151 : nat -> t
+| C_152 : nat -> t
+| C_153 : nat -> t
+| C_154 : nat -> t
+| C_155 : nat -> t
+| C_156 : nat -> t
+| C_157 : nat -> t
+| C_158 : nat -> t
+| C_159 : nat -> t
+| C_160 : nat -> t
+| C_161 : nat -> t
+| C_162 : nat -> t
+| C_163 : nat -> t
+| C_164 : nat -> t
+| C_165 : nat -> t
+| C_166 : nat -> t
+| C_167 : nat -> t
+| C_168 : nat -> t
+| C_169 : nat -> t
+| C_170 : nat -> t
+| C_171 : nat -> t
+| C_172 : nat -> t
+| C_173 : nat -> t
+| C_174 : nat -> t
+| C_175 : nat -> t
+| C_176 : nat -> t
+| C_177 : nat -> t
+| C_178 : nat -> t
+| C_179 : nat -> t
+| C_180 : nat -> t
+| C_181 : nat -> t
+| C_182 : nat -> t
+| C_183 : nat -> t
+| C_184 : nat -> t
+| C_185 : nat -> t
+| C_186 : nat -> t
+| C_187 : nat -> t
+| C_188 : nat -> t
+| C_189 : nat -> t
+| C_190 : nat -> t
+| C_191 : nat -> t
+| C_192 : nat -> t
+| C_193 : nat -> t
+| C_194 : nat -> t
+| C_195 : nat -> t
+| C_196 : nat -> t
+| C_197 : nat -> t
+| C_198 : nat -> t
+| C_199 : nat -> t
+| C_200 : nat -> t
+| C_201 : nat -> t
+| C_202 : nat -> t
+| C_203 : nat -> t
+| C_204 : nat -> t
+| C_205 : nat -> t
+| C_206 : nat -> t
+| C_207 : nat -> t
+| C_208 : nat -> t
+| C_209 : nat -> t
+| C_210 : nat -> t
+| C_211 : nat -> t
+| C_212 : nat -> t
+| C_213 : nat -> t
+| C_214 : nat -> t
+| C_215 : nat -> t
+| C_216 : nat -> t
+| C_217 : nat -> t
+| C_218 : nat -> t
+| C_219 : nat -> t
+| C_220 : nat -> t
+| C_221 : nat -> t
+| C_222 : nat -> t
+| C_223 : nat -> t
+| C_224 : nat -> t
+| C_225 : nat -> t
+| C_226 : nat -> t
+| C_227 : nat -> t
+| C_228 : nat -> t
+| C_229 : nat -> t
+| C_230 : nat -> t
+| C_231 : nat -> t
+| C_232 : nat -> t
+| C_233 : nat -> t
+| C_234 : nat -> t
+| C_235 : nat -> t
+| C_236 : nat -> t
+| C_237 : nat -> t
+| C_238 : nat -> t
+| C_239 : nat -> t
+| C_240 : nat -> t
+| C_241 : nat -> t
+| C_242 : nat -> t
+| C_243 : nat -> t
+| C_244 : nat -> t
+| C_245 : nat -> t
+| C_246 : nat -> t
+| C_247 : nat -> t
+| C_248 : nat -> t
+| C_249 : nat -> t
+| C_250 : nat -> t
+| C_251 : nat -> t
+| C_252 : nat -> t
+| C_253 : nat -> t
+| C_254 : nat -> t
+| C_255 : nat -> t
+| C_256 : nat -> t.
+
+Definition is_256 (x : t) : bool :=
+ match x with
+ | C_256 _ => true
+ | _ => false
+ end.
+
+Lemma falso : False.
+ assert (is_256 (C_256 0) = true) by reflexivity.
+ (* The next line was successful in 8.2pl3 *)
+ Fail assert (is_256 (C_256 0) = false) by (vm_compute; reflexivity).
+Abort.
diff --git a/test-suite/bugs/closed/bug_9663.v b/test-suite/bugs/closed/bug_9663.v
new file mode 100644
index 0000000000..b5fa601278
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9663.v
@@ -0,0 +1,2 @@
+Definition id_depfn S T (f : forall x : S, T x) := f.
+Definition idn : nat -> nat := @id_depfn _ _ (fun x => x).
diff --git a/test-suite/ssr/elim_noquant.v b/test-suite/ssr/elim_noquant.v
new file mode 100644
index 0000000000..e6662203e9
--- /dev/null
+++ b/test-suite/ssr/elim_noquant.v
@@ -0,0 +1,29 @@
+Require Import ssreflect.
+
+
+Axiom app : forall T, list T -> list T -> list T.
+Arguments app {_}.
+Infix "++" := app.
+
+Lemma test (aT rT : Type)
+ (pmap : (aT -> option rT) -> list aT -> list rT)
+ (perm_eq : list rT -> list rT -> Prop)
+ (f : aT -> option rT)
+ (g : rT -> aT)
+ (s t : list aT)
+ (E : forall T : list aT -> Type,
+ (forall s1 s2 s3 : list aT,
+ T (s1 ++ s2 ++ s3) -> T (s2 ++ s1 ++ s3)) ->
+ T s -> T t) :
+ perm_eq (pmap f s) (pmap f t).
+Proof.
+elim/E: (t).
+Admitted.
+
+
+Lemma test2 (a b : nat) : a = b -> b = 1.
+Proof.
+elim.
+match goal with |- a = 1 => idtac end.
+Admitted.
+
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 1981e24ae4..61b8cc3dcb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -31,7 +31,7 @@ open Entries
let refine_instance = ref false
let () = Goptions.(declare_bool_option {
- optdepr = false;
+ optdepr = true;
optname = "definition of instances by refining";
optkey = ["Refine";"Instance";"Mode"];
optread = (fun () -> !refine_instance);
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 07:36:41 +0000