diff options
| -rw-r--r-- | .gitlab-ci.yml | 4 | ||||
| -rw-r--r-- | CHANGES.md | 4 | ||||
| -rw-r--r-- | dev/doc/critical-bugs | 16 | ||||
| -rwxr-xr-x | dev/tools/backport-pr.sh | 30 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 4 | ||||
| -rw-r--r-- | interp/constrintern.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 64 | ||||
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 17 | ||||
| -rw-r--r-- | plugins/ssr/ssripats.ml | 20 | ||||
| -rw-r--r-- | pretyping/classops.ml | 33 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 17 | ||||
| -rw-r--r-- | stm/stm.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_4157.v | 272 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_9663.v | 2 | ||||
| -rw-r--r-- | test-suite/ssr/elim_noquant.v | 29 |
19 files changed, 434 insertions, 125 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index aacd248c43..58be1e4524 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -466,7 +466,7 @@ test-suite:edge+trunk+make: - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - opam update - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind https://gitlab.camlcity.org/gerd/lib-findlib.git#gerd/optional-vmthreads + - opam pin add -n ocamlfind --dev - opam install num - eval $(opam env) # We avoid problems with warnings: @@ -492,7 +492,7 @@ test-suite:edge+trunk+dune: - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - opam update - opam install ocaml-variants=4.09.0+trunk - - opam pin add -n ocamlfind https://gitlab.camlcity.org/gerd/lib-findlib.git#gerd/optional-vmthreads + - opam pin add -n ocamlfind --dev - opam pin add dune --dev # ounit lablgtk conf-gtksourceview - opam install dune num - eval $(opam env) diff --git a/CHANGES.md b/CHANGES.md index 4a66fa423e..dcf321c7ff 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -149,6 +149,10 @@ 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. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: 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/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/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 18cafd1f21..695dea222f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1430,8 +1430,8 @@ with the same physical-to-logical translation and with an empty logical prefix. The command line option ``-R`` is a variant of ``-Q`` which has the strictly same behavior regarding loadpaths, but which also makes the corresponding ``.vo`` files available through their short names in a way -not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R`` `path` ``Lib`` -associates to the file path `path`\ ``/path/fOO/Bar/File.vo`` the logical name +not unlike the ``Import`` command (see :ref:`here <import_qualid>`). For instance, ``-R path Lib`` +associates to the file ``/path/fOO/Bar/File.vo`` the logical name ``Lib.fOO.Bar.File``, but allows this file to be accessed through the short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with identical base name are present in different subdirectories of a 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/interp/constrintern.ml b/interp/constrintern.ml index 5ede9d6a99..349402035c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -956,7 +956,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (str "variable " ++ Id.print id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) - let _ = Context.Named.lookup id namedctx in + let _ = Environ.lookup_named_ctxt id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -1095,7 +1095,8 @@ let interp_reference vars r = let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None) {ids = Id.Set.empty; unb = false ; - tmp_scope = None; scopes = []; impls = empty_internalization_env} [] + tmp_scope = None; scopes = []; impls = empty_internalization_env} + Environ.empty_named_context_val (vars, Id.Map.empty) None [] r in r @@ -1826,7 +1827,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> let (c,imp,subscopes,l),_ = - intern_applied_reference intern env (Environ.named_context globalenv) + intern_applied_reference intern env (Environ.named_context_val globalenv) lvar us [] ref in apply_impargs c env imp subscopes l loc @@ -1932,7 +1933,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CAppExpl ((isproj,ref,us), args) -> let (f,_,args_scopes,_),args = let args = List.map (fun a -> (a,None)) args in - intern_applied_reference intern env (Environ.named_context globalenv) + intern_applied_reference intern env (Environ.named_context_val globalenv) lvar us args ref in (* Rem: GApp(_,f,[]) stands for @f *) @@ -1950,7 +1951,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = match f.CAst.v with | CRef (ref,us) -> intern_applied_reference intern env - (Environ.named_context globalenv) lvar us args ref + (Environ.named_context_val globalenv) lvar us args ref | CNotation (ntn,([],[],[],[])) -> let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in let x, impl, scopes, l = find_appl_head_data c in 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. + |