diff options
44 files changed, 421 insertions, 159 deletions
diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst new file mode 100644 index 0000000000..6a431f85ed --- /dev/null +++ b/doc/changelog/02-specification-language/13188-instance-gen.rst @@ -0,0 +1,6 @@ +- **Removed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. + Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 + <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst new file mode 100644 index 0000000000..eaf049dc97 --- /dev/null +++ b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst @@ -0,0 +1,6 @@ +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 <https://github.com/coq/coq/pull/13387>`_, + fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst new file mode 100644 index 0000000000..048835a0e9 --- /dev/null +++ b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst @@ -0,0 +1,6 @@ +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@@`; this covers for instance the case + :g:`r.(@@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst new file mode 100644 index 0000000000..089647a4b2 --- /dev/null +++ b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Avoiding exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern would break a dependency + (`#13337 <https://github.com/coq/coq/pull/13337>`_, + fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst new file mode 100644 index 0000000000..c02129a33f --- /dev/null +++ b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst @@ -0,0 +1,6 @@ +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 <https://github.com/coq/coq/pull/13373>`_, + fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst new file mode 100644 index 0000000000..a51f96d0a2 --- /dev/null +++ b/doc/changelog/04-tactics/13381-bfs_eauto.rst @@ -0,0 +1,6 @@ +- **Deprecated:** + Undocumented :n:`eauto @int_or_var @int_or_var` syntax in favor of new ``bfs eauto``. + Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``; + replacement TBD. + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst new file mode 100644 index 0000000000..1c7c3102a3 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 <https://github.com/coq/coq/pull/12516>`_, + by Maxime Dénès). diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 56d90b33d8..2474c784b8 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -391,6 +391,16 @@ Summary of the commands equivalent to ``Hint Resolve ident : typeclass_instances``, except it registers instances for :cmd:`Print Instances`. + .. flag:: Instance Generalized Output + + .. deprecated:: 8.13 + + Disabled by default, this provides compatibility with Coq + version 8.12 and earlier. + + When enabled, the type of the instance is implicitly generalized + over unbound and :ref:`generalizable <implicit-generalization>` variables as though surrounded by ``\`{}``. + .. cmd:: Print Instances @reference Shows the list of instances associated with the typeclass :token:`reference`. diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index fd8a0329d6..40d032543f 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -288,12 +288,18 @@ Name a set of section hypotheses for ``Proof using`` existential variables remain. To instantiate existential variables during proof edition, you should use the tactic :tacn:`instantiate`. + .. deprecated:: 8.13 + .. cmd:: Grab Existential Variables This command can be run when a proof has no more goal to be solved but has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. + .. deprecated:: 8.13 + + Use :cmd:`Unshelve` instead. + Proof modes ``````````` diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index a787d769fb..033ece04de 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1623,6 +1623,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "dfs" "eauto" OPT int_or_var auto_using hintbases +| "bfs" "eauto" OPT int_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 26474d950a..e6fc6188b7 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1754,6 +1754,7 @@ simple_tactic: [ | "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases | "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 378617af04..02c3c047d5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2092,9 +2092,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = assert (Option.is_empty isproj); let c = intern_notation intern env ntnvars loc ntn ntnargs in find_appl_head_data c, args - | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in - apply_impargs c env impargs args_scopes - args loc + | _ -> + assert (Option.is_empty isproj); + let f = intern_no_implicit env f in + let f, _, args_scopes = find_appl_head_data f in + (f,[],args_scopes), args + in + apply_impargs c env impargs args_scopes args loc | CRecord fs -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in diff --git a/interp/notation.ml b/interp/notation.ml index 8d05fab63c..948ebe9640 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -2035,12 +2035,12 @@ type symbol = | Break of int let rec symbol_eq s1 s2 = match s1, s2 with -| Terminal s1, Terminal s2 -> String.equal s1 s2 -| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2 -| SProdList (id1, l1), SProdList (id2, l2) -> - Id.equal id1 id2 && List.equal symbol_eq l1 l2 -| Break i1, Break i2 -> Int.equal i1 i2 -| _ -> false + | Terminal s1, Terminal s2 -> String.equal s1 s2 + | NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2 + | SProdList (id1, l1), SProdList (id2, l2) -> + Id.equal id1 id2 && List.equal symbol_eq l1 l2 + | Break i1, Break i2 -> Int.equal i1 i2 + | _ -> false let rec string_of_symbol = function | NonTerminal _ -> ["_"] @@ -2202,23 +2202,114 @@ let rec raw_analyze_notation_tokens = function | WhiteSpace n :: sl -> Break n :: raw_analyze_notation_tokens sl -let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn) - -let possible_notations ntn = +let rec raw_analyze_anonymous_notation_tokens = function + | [] -> [] + | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_anonymous_notation_tokens sl + | String "_" :: sl -> NonTerminal (Id.of_string "dummy") :: raw_analyze_anonymous_notation_tokens sl + | String s :: sl -> + Terminal (String.drop_simple_quotes s) :: raw_analyze_anonymous_notation_tokens sl + | WhiteSpace n :: sl -> raw_analyze_anonymous_notation_tokens sl + +(* Interpret notations with a recursive component *) + +let out_nt = function NonTerminal x -> x | _ -> assert false + +let msg_expected_form_of_recursive_notation = + "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." + +let rec find_pattern nt xl = function + | Break n as x :: l, Break n' :: l' when Int.equal n n' -> + find_pattern nt (x::xl) (l,l') + | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' -> + find_pattern nt (x::xl) (l,l') + | [], NonTerminal x' :: l' -> + (out_nt nt,x',List.rev xl),l' + | _, Break s :: _ | Break s :: _, _ -> + user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) + | _, Terminal s :: _ | Terminal s :: _, _ -> + user_err ~hdr:"Metasyntax.find_pattern" + (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") + | _, [] -> + user_err Pp.(str msg_expected_form_of_recursive_notation) + | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> + anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.") + +let rec interp_list_parser hd = function + | [] -> [], List.rev hd + | NonTerminal id :: tl when Id.equal id Notation_ops.ldots_var -> + if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); + let hd = List.rev hd in + let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in + let xyl,tl'' = interp_list_parser [] tl' in + (* We remember each pair of variable denoting a recursive part to *) + (* remove the second copy of it afterwards *) + (x,y)::xyl, SProdList (x,sl) :: tl'' + | (Terminal _ | Break _) as s :: tl -> + if List.is_empty hd then + let yl,tl' = interp_list_parser [] tl in + yl, s :: tl' + else + interp_list_parser (s::hd) tl + | NonTerminal _ as x :: tl -> + let xyl,tl' = interp_list_parser [x] tl in + xyl, List.rev_append hd tl' + | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.") + +let get_notation_vars l = + List.map_filter (function NonTerminal id | SProdList (id,_) -> Some id | _ -> None) l + +let decompose_raw_notation ntn = + let l = split_notation_string ntn in + let l = raw_analyze_notation_tokens l in + let recvars,l = interp_list_parser [] l in + let vars = get_notation_vars l in + recvars, vars, l + +let interpret_notation_string ntn = (* We collect the possible interpretations of a notation string depending on whether it is in "x 'U' y" or "_ U _" format *) let toks = split_notation_string ntn in - if List.exists (function String "_" -> true | _ -> false) toks then - (* Only "_ U _" format *) - [ntn] - else - let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in - if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn'] + let toks = + if + List.exists (function String "_" -> true | _ -> false) toks || + List.for_all (function String id -> Id.is_valid id | _ -> false) toks + then + (* Only "_ U _" format *) + raw_analyze_anonymous_notation_tokens toks + else + (* Includes the case of only a subset of tokens or an "x 'U' y"-style format *) + raw_analyze_notation_tokens toks + in + let _,toks = interp_list_parser [] toks in + let _,ntn' = make_notation_key None toks in + ntn' + +(* Tell if a non-recursive notation is an instance of a recursive one *) +let is_approximation ntn ntn' = + let rec aux toks1 toks2 = match (toks1, toks2) with + | Terminal s1 :: toks1, Terminal s2 :: toks2 -> String.equal s1 s2 && aux toks1 toks2 + | NonTerminal _ :: toks1, NonTerminal _ :: toks2 -> aux toks1 toks2 + | SProdList (_,l1) :: toks1, SProdList (_, l2) :: toks2 -> aux l1 l2 && aux toks1 toks2 + | NonTerminal _ :: toks1, SProdList (_,l2) :: toks2 -> aux' toks1 l2 l2 toks2 || aux toks1 toks2 + | [], [] -> true + | (Break _ :: _, _) | (_, Break _ :: _) -> assert false + | (Terminal _ | NonTerminal _ | SProdList _) :: _, _ -> false + | [], _ -> false + and aux' toks1 l2 l2full toks2 = match (toks1, l2) with + | Terminal s1 :: toks1, Terminal s2 :: l2 when String.equal s1 s2 -> aux' toks1 l2 l2full toks2 + | NonTerminal _ :: toks1, [] -> aux' toks1 l2full l2full toks2 || aux toks1 toks2 + | _ -> false + in + let _,toks = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn)) in + let _,toks' = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn')) in + aux toks toks' let browse_notation strict ntn map = - let ntns = possible_notations ntn in - let find (from,ntn' as fullntn') ntn = - if String.contains ntn ' ' then String.equal ntn ntn' + let ntn = interpret_notation_string ntn in + let find (from,ntn' as fullntn') = + if String.contains ntn ' ' then + if String.string_contains ~where:ntn' ~what:".." then is_approximation ntn ntn' + else String.equal ntn ntn' else let _,toks = decompose_notation_key fullntn' in let get_terminals = function Terminal ntn -> Some ntn | _ -> None in @@ -2230,7 +2321,7 @@ let browse_notation strict ntn map = String.Map.fold (fun scope_name sc -> NotationMap.fold (fun ntn data l -> - if List.exists (find ntn) ntns + if find ntn then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l else l) sc.notations) map [] in diff --git a/interp/notation.mli b/interp/notation.mli index b8939ff87b..97955bf92e 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -334,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool val make_notation_key : notation_entry -> symbol list -> notation val decompose_notation_key : notation -> notation_entry * symbol list -(** Decompose a notation of the form "a 'U' b" *) -val decompose_raw_notation : string -> symbol list +(** Decompose a notation of the form "a 'U' b" together with the lists + of pairs of recursive variables and the list of all variables + binding in the notation *) +val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list (** Prints scopes (expects a pure aconstr printer) *) val pr_scope_class : scope_class -> Pp.t diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 15861d49be..7e8400910c 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -116,12 +116,25 @@ END let make_depth n = snd (Eauto.make_dimension n None) +(* deprecated in 8.13; the second int_or_var will be removed *) +let deprecated_eauto_bfs = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.") + +let deprecated_bfs tacname = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.") + } TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () ); + Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND new_eauto @@ -135,13 +148,17 @@ END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND dfs_eauto @@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } END +TACTIC EXTEND bfs_eauto +| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db } +END + TACTIC EXTEND autounfold | [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index ecfe6c1664..236de65462 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -450,6 +450,11 @@ GRAMMAR EXTEND Gram ; as_or_and_ipat: [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat } + | "as"; ipat = equality_intropattern -> + { match ipat with + | IntroRewrite _ -> user_err Pp.(str "Disjunctive/conjunctive pattern expected.") + | IntroInjection _ -> user_err Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.") + | _ -> assert false } | -> { None } ] ] ; eqn_ipat: diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cbf539c1e9..00d4c7b3d8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1620,12 +1620,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = in Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 when app_empty -> + | Evar (evk1,_ as ev1), Evar ev2 when app_empty -> (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) - Success (solve_evar_evar ~force:true + (try + Success (solve_evar_evar ~force:true (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) + with IllTypedInstance (env,t,u) -> + UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))) | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 715b80f428..c58ebe1bbd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -810,7 +810,8 @@ let check_evar_instance unify flags env evd evk1 body = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) + with Retyping.RetypeError _ -> + let loc, _ = evi.evar_source in user_err ?loc (Pp.(str "Ill-typed evar instance")) in match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd @@ -1575,7 +1576,7 @@ let rec invert_definition unify flags choose imitate_defs match EConstr.kind !evdref t with | Rel i when i>k -> let open Context.Rel.Declaration in - (match Environ.lookup_rel (i-k) env' with + (match Environ.lookup_rel i env' with | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 8ff2d7fc63..094dae4828 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind -> Preconditions: - [ev] does not occur in [c]. - [c] does not contain any Meta(_) - *) + + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map @@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is - true); fails if the instance is not valid for the given [ev] *) + true); fails if the instance is not valid for the given [ev]; + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map @@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map + (** The two evars are expected to be in inferably convertible types; + if not, an exception IllTypedInstance is raised *) val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result @@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * types * types -(* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map + (** May raise IllTypedInstance if types are not convertible *) val remove_instance_local_defs : evar_map -> Evar.t -> 'a list -> 'a list diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 982814fdfc..c352a6ac1f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -38,7 +38,7 @@ type metabinding = (metavariable * EConstr.constr * (instance_constraint * insta type subst0 = (evar_map * metabinding list * - (Environ.env * EConstr.existential * EConstr.t) list) + ((Environ.env * int) * EConstr.existential * EConstr.t) list) module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -227,7 +227,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst : subst0) | Evar ev -> let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst + sigma,metasubst,((env,nb),ev,solve_pattern_eqn env sigma l c)::evarsubst | _ -> assert false let push d (env,n) = (push_rel_assum d env,n+1) @@ -769,21 +769,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | Some sigma -> sigma, metasubst, evarsubst | None -> - sigma,metasubst,((curenv,ev,cN)::evarsubst) + sigma,metasubst,((curenvnb,ev,cN)::evarsubst) end | Evar (evk,_ as ev), _ when is_evar_allowed flags evk && not (occur_evar sigma evk cN) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cnvars cmvars then - sigma,metasubst,((curenv,ev,cN)::evarsubst) + sigma,metasubst,((curenvnb,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) when is_evar_allowed flags evk && not (occur_evar sigma evk cM) -> let cmvars = free_rels sigma cM and cnvars = free_rels sigma cN in if Int.Set.subset cmvars cnvars then - sigma,metasubst,((curenv,ev,cM)::evarsubst) + sigma,metasubst,((curenvnb,ev,cM)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | Sort s1, Sort s2 -> (try @@ -1357,7 +1357,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = (* Process evars *) match evars with - | (curenv,(evk,_ as ev),rhs)::evars' -> + | ((curenv,nb),(evk,_ as ev),rhs)::evars' -> if Evd.is_defined evd evk then let v = mkEvar ev in let (evd,metas',evars'') = @@ -1376,7 +1376,8 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = w_merge_rec evd' metas evars eqns else let evd' = - let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in + let env' = pop_rel_context nb curenv in + let evd', rhs'' = pose_all_metas_as_evars env' evd rhs' in try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev,rhs'') diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 5462e09359..077597c278 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -105,7 +105,7 @@ type metabinding = (metavariable * constr * (instance_constraint * instance_typi type subst0 = (evar_map * metabinding list * - (Environ.env * existential * t) list) + ((Environ.env * int) * existential * t) list) val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map diff --git a/proofs/proof.ml b/proofs/proof.ml index d864aed25a..24f3ac3f29 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -409,14 +409,28 @@ module V82 = struct let top_evars p = Proofview.V82.top_evars p.entry p.proofview + let warn_deprecated_grab_existentials = + CWarnings.create ~name:"deprecated-grab-existentials" ~category:"deprecated" + Pp.(fun () -> str "The Grab Existential Variables command is " ++ + str"deprecated. Please use the Unshelve command or the unshelve tactical " ++ + str"instead.") + let grab_evars p = + warn_deprecated_grab_existentials (); if not (is_done p) then raise (OpenProof(None, UnfinishedProof)) else { p with proofview = Proofview.V82.grab p.proofview } + let warn_deprecated_existential = + CWarnings.create ~name:"deprecated-existential" ~category:"deprecated" + Pp.(fun () -> str "The Existential command is " ++ + str"deprecated. Please use the Unshelve command or the unshelve " ++ + str"tactical, and the instantiate tactic instead.") + (* Main component of vernac command Existential *) let instantiate_evar env n intern pr = + warn_deprecated_existential (); let tac = Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> let (evk, evi) = diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 5fb038a767..f40bbc813e 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -30,4 +30,5 @@ val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic val autounfold_one : hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic +val make_depth : int option -> int val make_dimension : int option -> int option -> bool * int diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f3ecc2a9f0..e3369bc9be 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -198,22 +198,24 @@ let clear_in_global_msg = function | Some ref -> str " implicitly in " ++ Printer.pr_global ref let clear_dependency_msg env sigma id err inglobal = + let ppidupper = function Some id -> Id.print id | None -> str "This variable" in + let ppid = function Some id -> Id.print id | None -> str "this variable" in let pp = clear_in_global_msg inglobal in match err with | Evarutil.OccurHypInSimpleClause None -> - Id.print id ++ str " is used" ++ pp ++ str " in conclusion." + ppidupper id ++ str " is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." + ppidupper id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> - str "Cannot remove " ++ Id.print id ++ + str "Cannot remove " ++ ppid id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." | Evarutil.NoCandidatesLeft ev -> - str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++ + str "Cannot remove " ++ ppid id ++ str " as it would leave the existential " ++ Printer.pr_existential_key sigma ev ++ str" without candidates." let error_clear_dependency env sigma id err inglobal = - user_err (clear_dependency_msg env sigma id err inglobal) + user_err (clear_dependency_msg env sigma (Some id) err inglobal) let replacing_dependency_msg env sigma id err inglobal = let pp = clear_in_global_msg inglobal in @@ -2130,7 +2132,9 @@ let clear_body ids = end let clear_wildcards ids = - Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear [id]) ids + let clear_wildcards_msg ?loc env sigma _id err inglobal = + user_err ?loc (clear_dependency_msg env sigma None err inglobal) in + Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear_gen (clear_wildcards_msg ?loc) [id]) ids (* Takes a list of booleans, and introduces all the variables * quantified in the goal which are associated with a value diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v new file mode 100644 index 0000000000..93ba6f17e0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12348.v @@ -0,0 +1,11 @@ +(* Was raising an anomaly before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := _ in + (fun n : nat => 0 : X) : _. + +(* Was raising an ill-typed instance error before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := true in + (fun n : nat => 0 : X) : _. diff --git a/test-suite/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v new file mode 100644 index 0000000000..cc11aa93b6 --- /dev/null +++ b/test-suite/bugs/closed/bug_13363.v @@ -0,0 +1,17 @@ +Axiom X : Type. +Axiom P : (X -> unit) -> Prop. + +Axiom F: unit -> unit. +Axiom G : unit -> unit. + +Lemma Hyp ss': + P (fun y : X => ss') -> + P (fun y : X => G (F ss')). +Admitted. + +Lemma bug : exists x, P x. +Proof. +intros. +eexists (fun y : X => G _). +eapply Hyp. cbn beta. +Abort. diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v index 462a615d91..f3a19c2b89 100644 --- a/test-suite/bugs/closed/bug_3513.v +++ b/test-suite/bugs/closed/bug_3513.v @@ -13,7 +13,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v index d667022e68..2d4d7d02cc 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -15,7 +15,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v new file mode 100644 index 0000000000..f885e31352 --- /dev/null +++ b/test-suite/bugs/closed/bug_5512.v @@ -0,0 +1,10 @@ +(* Check that an anomaly is not raised *) +(* It should however eventually succeed... *) +Goal exists x, x. +Proof. +simple refine (ex_intro _ _ _). +shelve. +(* The failure is due to Type(u)<=Prop for u an arbitrary sort + variable being rejected *) +Fail simple refine (_ _). +Abort. diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v new file mode 100644 index 0000000000..72f612560b --- /dev/null +++ b/test-suite/bugs/closed/bug_6042.v @@ -0,0 +1,7 @@ +Class C (n: nat) := T{x:True}. +Generalizable All Variables. + +Fail Instance i : C n. + +Instance i : `(C n). +Proof. repeat constructor. Defined. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 70427220ed..3f07261ca6 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -7,3 +7,5 @@ H is already used. The command has indeed failed with message: H is already used. a +The command has indeed failed with message: +This variable is used in hypothesis H. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 96b6d652c9..8526e43a23 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -30,3 +30,11 @@ Goal True. assert_succeeds should_not_loop. assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) Abort. + +Module IntroWildcard. + +Theorem foo : { p:nat*nat & p = (0,0) } -> True. +Fail intros ((n,_),H). +Abort. + +End IntroWildcard. diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,8 @@ Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) Notation "x && y" := (andb x y) : bool_scope +Notation "'U' t" := (S t) (default interpretation) +Notation "'_' t" := (S t) (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index af8b0ee193..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,26 @@ Set Printing Width 400. Notation "b1 && b2" := (if b1 then b2 else false). Locate "&&". + +Module M. + +Notation "'U' t" := (S t) (at level 0). +Notation "'_' t" := (S t) (at level 0). +Locate "U". (* was wrongly returning also "'_' t" *) +Locate "_". + +End M. + +Module N. + +(* Was not working at some time *) +Locate "( t , u , .. , v )". + +(* Was working though *) +Locate "( _ , _ , .. , _ )". + +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + +End N. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 382c252727..fb8bbfd043 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -51,8 +51,8 @@ Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ Notation c3 x := ((@pair') _ x). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *) Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) -Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) -Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. +Check c3 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c3 0 y 0 => 2 | _ => 1 end. (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) (* unless an atomic @ is given *) diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 06697af901..8b7d239dcd 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -26,3 +26,15 @@ Definition c := ε : U. Goal True. assert (nat * nat). Abort. + +(* Check propagation of scopes in indirect applications to references *) + +Module PropagateIndirect. +Notation "0" := true : bool_scope. + +Axiom f : bool -> bool -> nat. +Check (@f 0) 0. + +Record R := { p : bool -> nat }. +Check fun r => r.(@p) 0. +End PropagateIndirect. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 892568c3d8..9ff18ebe2c 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -1,4 +1,4 @@ -(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.CMorphisms") -*- *) +(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.CMorphisms") -*- *) (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) @@ -316,7 +316,7 @@ Section GenericInstances. Global Program Instance trans_contra_inv_impl_type_morphism - `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3. + `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -326,7 +326,7 @@ Section GenericInstances. Global Program Instance trans_co_impl_type_morphism - `(Transitive A R) : Proper (R ++> arrow) (R x) | 3. + `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -336,7 +336,7 @@ Section GenericInstances. Global Program Instance trans_sym_co_inv_impl_type_morphism - `(PER A R) : Proper (R ++> flip arrow) (R x) | 3. + `(PER A R) {x} : Proper (R ++> flip arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -345,7 +345,7 @@ Section GenericInstances. Qed. Global Program Instance trans_sym_contra_arrow_morphism - `(PER A R) : Proper (R --> arrow) (R x) | 3. + `(PER A R) {x} : Proper (R --> arrow) (R x) | 3. Next Obligation. Proof with auto. @@ -354,7 +354,7 @@ Section GenericInstances. Qed. Global Program Instance per_partial_app_type_morphism - `(PER A R) : Proper (R ==> iffT) (R x) | 2. + `(PER A R) {x} : Proper (R ==> iffT) (R x) | 2. Next Obligation. Proof with auto. @@ -407,17 +407,17 @@ Section GenericInstances. (** Coq functions are morphisms for Leibniz equality, applied only if really needed. *) - Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') {A} : Reflexive (@Logic.eq A ==> R'). Proof. simpl_crelation. Qed. (** [respectful] is a morphism for crelation equivalence . *) - Global Instance respectful_morphism : + Global Instance respectful_morphism {A B} : Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). Proof. - intros A B R R' HRR' S S' HSS' f g. + intros R R' HRR' S S' HSS' f g. unfold respectful , relation_equivalence in *; simpl in *. split ; intros H x y Hxy. - apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). @@ -519,9 +519,9 @@ Ltac partial_application_tactic := (** Bootstrap !!! *) -Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). +Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). Proof. - intros A R R' HRR' x y <-. red in HRR'. + intros R R' HRR' x y <-. red in HRR'. split ; red ; intros. - now apply (fst (HRR' _ _)). - now apply (snd (HRR' _ _)). diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index ffbea7dddf..87abc4a08f 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,4 +1,4 @@ -(* -*- coding: utf-8; coq-prog-args: ("-coqlib" "../.." "-R" ".." "Coq" "-top" "Coq.Classes.Morphisms") -*- *) +(* -*- coding: utf-8; coq-prog-args: ("-top" "Coq.Classes.Morphisms") -*- *) (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) @@ -317,7 +317,7 @@ Section GenericInstances. Global Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. + `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3. Next Obligation. Proof with auto. @@ -327,7 +327,7 @@ Section GenericInstances. Global Program Instance trans_co_impl_morphism - `(Transitive A R) : Proper (R ++> impl) (R x) | 3. + `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -337,7 +337,7 @@ Section GenericInstances. Global Program Instance trans_sym_co_inv_impl_morphism - `(PER A R) : Proper (R ++> flip impl) (R x) | 3. + `(PER A R) {x} : Proper (R ++> flip impl) (R x) | 3. Next Obligation. Proof with auto. @@ -346,7 +346,7 @@ Section GenericInstances. Qed. Global Program Instance trans_sym_contra_impl_morphism - `(PER A R) : Proper (R --> impl) (R x) | 3. + `(PER A R) {x} : Proper (R --> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -355,7 +355,7 @@ Section GenericInstances. Qed. Global Program Instance per_partial_app_morphism - `(PER A R) : Proper (R ==> iff) (R x) | 2. + `(PER A R) {x} : Proper (R ==> iff) (R x) | 2. Next Obligation. Proof with auto. @@ -528,9 +528,9 @@ Ltac partial_application_tactic := (** Bootstrap !!! *) -Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). +Instance proper_proper {A} : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). Proof. - intros A x y H y0 y1 e; destruct e. + intros x y H y0 y1 e; destruct e. reduce in H. split ; red ; intros H0. - setoid_rewrite <- H. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index a168a8e7cd..964786d8e6 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -22,11 +22,11 @@ Generalizable Variables A l. (** Morphisms for relations *) -Instance relation_conjunction_morphism : Proper (relation_equivalence (A:=A) ==> +Instance relation_conjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_conjunction. Proof. firstorder. Qed. -Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> +Instance relation_disjunction_morphism {A} : Proper (relation_equivalence (A:=A) ==> relation_equivalence ==> relation_equivalence) relation_disjunction. Proof. firstorder. Qed. @@ -43,11 +43,11 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed. (** The instantiation at relation allows rewriting applications of relations [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) -Instance relation_equivalence_pointwise : +Instance relation_equivalence_pointwise {A} : Proper (relation_equivalence ==> pointwise_relation A (pointwise_relation A iff)) id. Proof. intro. apply (predicate_equivalence_pointwise (Tcons A (Tcons A Tnil))). Qed. -Instance subrelation_pointwise : +Instance subrelation_pointwise {A} : Proper (subrelation ==> pointwise_relation A (pointwise_relation A impl)) id. Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index d8246c22e1..54ee06343a 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -409,7 +409,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) -Program Instance predicate_equivalence_equivalence : +Program Instance predicate_equivalence_equivalence {l} : Equivalence (@predicate_equivalence l). Next Obligation. @@ -427,7 +427,7 @@ Program Instance predicate_equivalence_equivalence : firstorder. Qed. -Program Instance predicate_implication_preorder : +Program Instance predicate_implication_preorder {l} : PreOrder (@predicate_implication l). Next Obligation. intro l; induction l ; firstorder. @@ -495,7 +495,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and relation equivalence. *) -Program Instance subrelation_partial_order : +Program Instance subrelation_partial_order {A} : PartialOrder (@relation_equivalence A) subrelation. Next Obligation. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index afe69cae7f..87e66a25dd 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -61,11 +61,9 @@ Class Measure {A B} (f : A -> B). (** Standard measures. *) -Instance fst_measure : @Measure (A * B) A Fst. -Defined. +Instance fst_measure {A B} : @Measure (A * B) A Fst := {}. -Instance snd_measure : @Measure (A * B) B Snd. -Defined. +Instance snd_measure {A B} : @Measure (A * B) B Snd := {}. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) @@ -96,11 +94,11 @@ Section RelCompFun_Instances. `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). Proof. firstorder. Qed. - Global Program Instance RelCompFun_Equivalence - `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). + Global Instance RelCompFun_Equivalence + `(Measure A B f, Equivalence _ R) : Equivalence (R@@f) := {}. - Global Program Instance RelCompFun_StrictOrder - `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). + Global Instance RelCompFun_StrictOrder + `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f) := {}. End RelCompFun_Instances. diff --git a/theories/Compat/Coq812.v b/theories/Compat/Coq812.v index f52b559f84..992b00e834 100644 --- a/theories/Compat/Coq812.v +++ b/theories/Compat/Coq812.v @@ -11,4 +11,6 @@ (** Compatibility file for making Coq act similar to Coq v8.12 *) Require Export Coq.Compat.Coq813. +Local Set Warnings "-deprecated". Set Firstorder Solver auto with *. +Export Set Instance Generalized Output. diff --git a/vernac/classes.ml b/vernac/classes.ml index 054addc542..062cc90f8f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -502,9 +502,16 @@ let do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' else declare_instance_program pm env sigma ~global ~poly id pri imps decl term termtype -let interp_instance_context ~program_mode env ctx ~generalize pl tclass = +let auto_generalize = + Goptions.declare_bool_option_and_ref + ~depr:true + ~key:["Instance";"Generalized";"Output"] + ~value:false + +let interp_instance_context ~program_mode env ctx ?(generalize=auto_generalize()) pl tclass = let sigma, decl = interp_univ_decl_opt env pl in let tclass = + (* when we remove this code, we can remove the middle argument of CGeneralization *) if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass) else tclass in @@ -530,10 +537,10 @@ let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance_common ~program_mode ~generalize env instid ctx cl = +let new_instance_common ~program_mode ?generalize env instid ctx cl = let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ~generalize ctx pl cl + interp_instance_context ~program_mode env ?generalize ctx pl cl in (* The name generator should not be here *) let id = @@ -548,20 +555,20 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl = let new_instance_interactive ?(global=false) ~poly instid ctx cl - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook + ?generalize ?(tac:unit Proofview.tactic option) ?hook pri opt_props = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:false ~generalize env instid ctx cl in + new_instance_common ~program_mode:false ?generalize env instid ctx cl in id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props let new_instance_program ?(global=false) ~pm ~poly instid ctx cl opt_props - ?(generalize=true) ?hook pri = + ?generalize ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:true ~generalize env instid ctx cl in + new_instance_common ~program_mode:true ?generalize env instid ctx cl in let pm = do_instance_program ~pm env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props in @@ -569,10 +576,10 @@ let new_instance_program ?(global=false) ~pm let new_instance ?(global=false) ~poly instid ctx cl props - ?(generalize=true) ?hook pri = + ?generalize ?hook pri = let env = Global.env() in let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = - new_instance_common ~program_mode:false ~generalize env instid ctx cl in + new_instance_common ~program_mode:false ?generalize env instid ctx cl in do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props; id diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8477870cb4..dc2b2e889e 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -194,52 +194,6 @@ let parse_format ({CAst.loc;v=str} : lstring) = (***********************) (* Analyzing notations *) -(* Interpret notations with a recursive component *) - -let out_nt = function NonTerminal x -> x | _ -> assert false - -let msg_expected_form_of_recursive_notation = - "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"." - -let rec find_pattern nt xl = function - | Break n as x :: l, Break n' :: l' when Int.equal n n' -> - find_pattern nt (x::xl) (l,l') - | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' -> - find_pattern nt (x::xl) (l,l') - | [], NonTerminal x' :: l' -> - (out_nt nt,x',List.rev xl),l' - | _, Break s :: _ | Break s :: _, _ -> - user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side.")) - | _, Terminal s :: _ | Terminal s :: _, _ -> - user_err ~hdr:"Metasyntax.find_pattern" - (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.") - | _, [] -> - user_err Pp.(str msg_expected_form_of_recursive_notation) - | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) -> - anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.") - -let rec interp_list_parser hd = function - | [] -> [], List.rev hd - | NonTerminal id :: tl when Id.equal id ldots_var -> - if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation); - let hd = List.rev hd in - let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in - let xyl,tl'' = interp_list_parser [] tl' in - (* We remember each pair of variable denoting a recursive part to *) - (* remove the second copy of it afterwards *) - (x,y)::xyl, SProdList (x,sl) :: tl'' - | (Terminal _ | Break _) as s :: tl -> - if List.is_empty hd then - let yl,tl' = interp_list_parser [] tl in - yl, s :: tl' - else - interp_list_parser (s::hd) tl - | NonTerminal _ as x :: tl -> - let xyl,tl' = interp_list_parser [x] tl in - xyl, List.rev_append hd tl' - | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.") - - (* Find non-terminal tokens of notation *) (* To protect alphabetic tokens and quotes from being seen as variables *) @@ -256,24 +210,16 @@ let is_numeral_in_constr entry symbs = | _ -> false -let rec get_notation_vars onlyprint = function - | [] -> [] - | NonTerminal id :: sl -> - let vars = get_notation_vars onlyprint sl in - if Id.equal id ldots_var then vars else - (* don't check for nonlinearity if printing only, see Bug 5526 *) - if not onlyprint && Id.List.mem id vars then - user_err ~hdr:"Metasyntax.get_notation_vars" - (str "Variable " ++ Id.print id ++ str " occurs more than once.") - else id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl - | SProdList _ :: _ -> assert false - -let analyze_notation_tokens ~onlyprint ntn = - let l = decompose_raw_notation ntn in - let vars = get_notation_vars onlyprint l in - let recvars,l = interp_list_parser [] l in - recvars, List.subtract Id.equal vars (List.map snd recvars), l +let analyze_notation_tokens ~onlyprint df = + let (recvars,mainvars,symbols as res) = decompose_raw_notation df in + (* don't check for nonlinearity if printing only, see Bug 5526 *) + (if not onlyprint then + match List.duplicates Id.equal (mainvars @ List.map snd recvars) with + | id :: _ -> + user_err ~hdr:"Metasyntax.get_notation_vars" + (str "Variable " ++ Id.print id ++ str " occurs more than once.") + | _ -> ()); + res let error_not_same_scope x y = user_err ~hdr:"Metasyntax.error_not_name_scope" |