diff options
| -rw-r--r-- | CHANGES.md | 4 | ||||
| -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_9663.v | 2 | ||||
| -rw-r--r-- | test-suite/ssr/elim_noquant.v | 29 |
16 files changed, 152 insertions, 115 deletions
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/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_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. + |