diff options
36 files changed, 459 insertions, 168 deletions
@@ -34,6 +34,7 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes - #4677: fix alpha-conversion in notations needing eta-expansion +- Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. Changes from V8.5 to V8.5pl1 ============================ diff --git a/checker/votour.ml b/checker/votour.ml index 79755da4a..48f9f45e7 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -10,6 +10,26 @@ open Values (** {6 Interactive visit of a vo} *) +let rec read_num max = + let quit () = + Printf.printf "\nGoodbye!\n%!"; + exit 0 in + Printf.printf "# %!"; + let l = try read_line () with End_of_file -> quit () in + if l = "u" then None + else if l = "x" then quit () + else + try + let v = int_of_string l in + if v < 0 || v >= max then + let () = + Printf.printf "Out-of-range input! (only %d children)\n%!" max in + read_num max + else Some v + with Failure "int_of_string" -> + Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!"; + read_num max + type 'a repr = | INT of int | STRING of string @@ -255,15 +275,13 @@ let rec visit v o pos = (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop)) children; Printf.printf "-------------\n"; - Printf.printf ("# %!"); - let l = read_line () in try - if l = "u" then let info = pop () in visit info.typ info.obj info.pos - else if l = "x" then (Printf.printf "\nGoodbye!\n\n";exit 0) - else - let v',o',pos' = children.(int_of_string l) in - push (get_name v) v o pos; - visit v' o' pos' + match read_num (Array.length children) with + | None -> let info = pop () in visit info.typ info.obj info.pos + | Some child -> + let v',o',pos' = children.(child) in + push (get_name v) v o pos; + visit v' o' pos' with | Failure "empty stack" -> () | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos @@ -350,13 +368,13 @@ let visit_vo f = let size = if Sys.word_size = 64 then header.size64 else header.size32 in Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size) segments; - Printf.printf "# %!"; - let l = read_line () in - let seg = int_of_string l in - seek_in ch segments.(seg).pos; - let o = Repr.input ch in - let () = Visit.init () in - Visit.visit segments.(seg).typ o [] + match read_num (Array.length segments) with + | Some seg -> + seek_in ch segments.(seg).pos; + let o = Repr.input ch in + let () = Visit.init () in + Visit.visit segments.(seg).typ o [] + | None -> () done let main = diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index f5a1bf3b2..54450fe7d 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2833,42 +2833,57 @@ This tactic is deprecated. It can be replaced by {\tt enough} \tacindex{subst} \optindex{Regular Subst Tactic} -This tactic applies to a goal that has \ident\ in its context and -(at least) one hypothesis, say {\tt H}, of type {\tt - \ident=t} or {\tt t=\ident}. Then it replaces -\ident\ by {\tt t} everywhere in the goal (in the hypotheses -and in the conclusion) and clears \ident\ and {\tt H} from the context. +This tactic applies to a goal that has \ident\ in its context and (at +least) one hypothesis, say $H$, of type {\tt \ident} = $t$ or $t$ +{\tt = \ident} with {\ident} not occurring in $t$. Then it replaces +{\ident} by $t$ everywhere in the goal (in the hypotheses and in the +conclusion) and clears {\ident} and $H$ from the context. + +If {\ident} is a local definition of the form {\ident} := $t$, it is +also unfolded and cleared. + +\Rem +When several hypotheses have the form {\tt \ident} = $t$ or {\tt + $t$ = \ident}, the first one is used. \Rem -When several hypotheses have the form {\tt \ident=t} or {\tt - t=\ident}, the first one is used. +If $H$ is itself dependent in the goal, it is replaced by the +proof of reflexivity of equality. \begin{Variants} - \item {\tt subst \ident$_1$ \dots \ident$_n$} + \item {\tt subst \ident$_1$ {\dots} \ident$_n$} - Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. + This is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}. \item {\tt subst} - Applies {\tt subst} repeatedly to all identifiers from the context - for which an equality exists. + This applies {\tt subst} repeatedly from top to bottom to all + identifiers of the context for which an equality of the form {\tt + \ident} = $t$ or $t$ {\tt = \ident} or {\tt \ident} := $t$ exists, with + {\ident} not occurring in $t$. -\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled using option {\tt Set - Regular Subst Tactic}. When this option is activated, {\tt subst} - manages the following corner cases which otherwise it - does not: +\noindent {\bf Remark: } The behavior of {\tt subst} can be controlled +using option {\tt Set Regular Subst Tactic}. When this option is +activated, {\tt subst} also deals with the following corner cases: \begin{itemize} \item A context with ordered hypotheses {\tt \ident$_1$ = \ident$_2$} and {\tt \ident$_1$ = $t$}, or {$t'$ = \ident$_1$} with $t'$ not a variable, and no other hypotheses of the form {\tt \ident$_2$ = $u$} - or {\tt $u$ = \ident$_2$} + or {\tt $u$ = \ident$_2$}; without the option, a second call to {\tt + subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ + respectively. + \item A context with cyclic dependencies as with hypotheses {\tt - \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} + \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which + without the option would be a cause of failure of {\tt subst}. \end{itemize} -Additionally, it prevents a local definition such as {\tt \ident := - $t$} to be unfolded which otherwise it would exceptionally unfold in +Additionally, it prevents a local definition such as {\tt \ident} := + $t$ to be unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form {\tt {\ident} = $u$}, or {\tt $u'$ = \ident} with $u'$ not a variable. +Finally, it preserves the initial order of hypotheses, which without +the option it may break. + The option is on by default. \end{Variants} diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 072af0779..0de98242a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -759,7 +759,15 @@ let intern_qualid loc qid intern env lvar us args = let subst = (terms, Id.Map.empty, Id.Map.empty) in let infos = (Id.Map.empty, env) in let projapp = match c with NRef _ -> true | _ -> false in - subst_aconstr_in_glob_constr loc intern lvar subst infos c, projapp, args2 + let c = subst_aconstr_in_glob_constr loc intern lvar subst infos c in + let c = match us, c with + | None, _ -> c + | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) + | Some _, _ -> + user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++ + str " cannot have a universe instance") + in + c, projapp, args2 (* Rule out section vars since these should have been found by intern_var *) let intern_non_secvar_qualid loc qid intern env lvar us args = diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 44a62ef37..85212b7ab 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -172,7 +172,7 @@ let cook_notation df sc = (* - all single quotes in terminal tokens are doubled *) (* - characters < 32 are represented by '^A, '^B, '^C, etc *) (* The output is decoded in function Index.prepare_entry of coqdoc *) - let ntn = String.make (String.length df * 3) '_' in + let ntn = String.make (String.length df * 5) '_' in let j = ref 0 in let l = String.length df - 1 in let i = ref 0 in diff --git a/library/declaremods.ml b/library/declaremods.ml index 4c9c40a73..701c15e14 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -727,7 +727,10 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = let arg_entries_r = intern_args interp_modast args in let params = mk_params_entry arg_entries_r in let env = Global.env () in - let entry = params, fst (interp_modast env ModType mty) in + let mte, _ = interp_modast env ModType mty in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in + let entry = params, mte in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in let sobjs = get_functor_sobjs false env inl entry in let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index a438ca79f..802c36109 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -24,17 +24,14 @@ open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in let env = Goal.V82.env sigma g in - let preamb,thesis,penv,pc = - (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - (str "thesis := " ++ fnl ()), - Printer.pr_context_of env sigma, - Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - preamb ++ - str" " ++ hv 0 (penv ++ fnl () ++ - str (Printer.emacs_str "") ++ - str "============================" ++ fnl () ++ - thesis ++ str " " ++ pc) ++ fnl () + let concl = Goal.V82.concl sigma g in + let goal = + Printer.pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + str "thesis :=" ++ cut () ++ + Printer.pr_goal_concl_style_env env sigma concl in + str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++ + str " " ++ v 0 goal let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = match gll with diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 6c57bc2bb..098f76bbf 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -285,7 +285,7 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ -> Tunknown + | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 713c99597..8b061e3c2 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -592,7 +592,7 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s) let lookup_eliminator ind_sp s = let kn,i = ind_sp in - let mp,dp,l = repr_mind kn in + let mp,dp,l = KerName.repr (MutInd.canonical kn) in let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in let id = add_suffix ind_id (elimination_suffix s) in (* Try first to get an eliminator defined in the same section as the *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 7f4249c5b..b6eb3a037 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -810,7 +810,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let fold () = let () = if !debug_RAKAM then let open Pp in pp (str "<><><><><>" ++ fnl ()) in - if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l) + (s,cst_l) in match kind_of_term x with | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA -> @@ -1001,7 +1001,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in - whrec (Option.default Cst_stack.empty csts) + fun xs -> + let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in + if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res (** reduction machine without global env and refold machinery *) let local_whd_state_gen flags sigma = diff --git a/printing/printer.ml b/printing/printer.ml index 22bc122bd..a16a92d0a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -384,16 +384,12 @@ let pr_transparent_state (ids, csts) = let default_pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in let env = Goal.V82.env sigma g in - let preamb,thesis,penv,pc = - mt (), mt (), - pr_context_of env sigma, - pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - preamb ++ - str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str "") ++ - str "============================" ++ fnl () ++ - thesis ++ str " " ++ pc) + let concl = Goal.V82.concl sigma g in + let goal = + pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + pr_goal_concl_style_env env sigma concl in + str " " ++ v 0 goal (* display a goal tag *) let pr_goal_tag g = diff --git a/stm/stm.ml b/stm/stm.ml index b25e88812..c296361a1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1840,7 +1840,7 @@ let known_state ?(redefine_qed=false) ~cache id = if ctac then Hooks.(call tactic_being_run true); vernac_interp id x; if ctac then Hooks.(call tactic_being_run false); - if eff then update_global_env ()), cache, true + if eff then update_global_env ()), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> reach view.next; vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () @@ -2248,13 +2248,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = vernac_interp (VCS.get_branch_pos head) x; `Ok | VtSideff l, w -> + let ceff_in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd {ctac=false;ceff=true;cast=x;cids=l;cqueue=`MainQueue}); let replay = match x.expr with | VernacDefinition(_, _, DefineBody _) -> None | _ -> Some x in + VCS.commit id (Cmd {ctac=false;ceff=ceff_in_proof;cast=x;cids=l;cqueue=`MainQueue}); VCS.propagate_sideff replay; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); `Ok diff --git a/tactics/equality.ml b/tactics/equality.ml index bc03baf26..cb1d82ae6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1610,6 +1610,17 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) +let regular_subst_tactic = ref true + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && not (is_global glob_identity eq) @@ -1638,24 +1649,25 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = - List.rev (snd (List.fold_right (fun dcl (deps,allhyps) -> + List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = get_id dcl in if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then - ((if is_local_assum dcl then deps else id::deps), id::allhyps) + let id_dest = if !regular_subst_tactic then dest else MoveLast in + (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps) else - (deps,allhyps)) + (MoveBefore id,deps,allhyps)) hyps - ([x],[]))) in + (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) let depconcl = occur_var env x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [revert dephyps; + [revert (List.map snd dephyps); general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); - (tclMAP intro_using dephyps)] + (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) @@ -1706,17 +1718,6 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -let regular_subst_tactic = ref true - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "more regular behavior of tactic subst"; - optkey = ["Regular";"Subst";"Tactic"]; - optread = (fun () -> !regular_subst_tactic); - optwrite = (:=) regular_subst_tactic } - let subst_all ?(flags=default_subst_tactic_flags ()) () = if !regular_subst_tactic then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a626092dd..0bb842601 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1836,19 +1836,19 @@ let on_the_bodies = function | [id] -> str " depends on the body of " ++ pr_id id | l -> str " depends on the bodies of " ++ pr_sequence pr_id l -let check_is_type env ty msg = - Proofview.tclEVARMAP >>= fun sigma -> +exception DependsOnBody of Id.t option + +let check_is_type env sigma ty = let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + raise (DependsOnBody None) -let check_decl env decl msg = +let check_decl env sigma decl = let open Context.Named.Declaration in let ty = get_type decl in - Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in @@ -1856,15 +1856,17 @@ let check_decl env decl msg = | LocalAssum _ -> () | LocalDef (_,c,_) -> Typing.e_check env evdref c ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + let id = get_id decl in + raise (DependsOnBody (Some id)) let clear_body ids = let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function | LocalAssum (id,t) as decl -> @@ -1878,23 +1880,32 @@ let clear_body ids = let ctx = List.map map ctx in let base_env = reset_context env in let env = push_named_context ctx base_env in - let check_hyps = - let check env decl = - let msg _ = Tacticals.New.tclZEROMSG - (str "Hypothesis " ++ pr_id (get_id decl) ++ on_the_bodies ids) + let check = + try + let check (env, sigma) decl = + (** Do no recheck hypotheses that do not depend *) + let sigma = + if List.exists (fun id -> occur_var_in_decl env id decl) ids then + check_decl env sigma decl + else sigma + in + (push_named decl env, sigma) in - check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env) - in - let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in - Proofview.tclIGNORE checks - in - let check_concl = - let msg _ = Tacticals.New.tclZEROMSG - (str "Conclusion" ++ on_the_bodies ids) - in - check_is_type env concl msg + let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in + let sigma = + if List.exists (fun id -> occur_var env id concl) ids then + check_is_type env sigma concl + else sigma + in + Proofview.Unsafe.tclEVARS sigma + with DependsOnBody where -> + let msg = match where with + | None -> str "Conclusion" ++ on_the_bodies ids + | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids + in + Tacticals.New.tclZEROMSG msg in - check_hyps <*> check_concl <*> + check <*> Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end } diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v new file mode 100644 index 000000000..e594b74b6 --- /dev/null +++ b/test-suite/bugs/closed/3825.v @@ -0,0 +1,16 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Axiom foo@{i j} : Type@{i} -> Type@{j}. + +Notation bar := foo. + +Monomorphic Universes i j. + +Check bar@{i j}. +Fail Check bar@{i}. + +Notation qux := (nat -> nat). + +Fail Check qux@{i}. + diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v index 5013bc6ac..d88e8c332 100644 --- a/test-suite/bugs/closed/3922.v +++ b/test-suite/bugs/closed/3922.v @@ -73,7 +73,7 @@ Definition Trunc_ind {n A} (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} : (forall a, P (tr a)) -> (forall aa, P aa) := (fun f aa => match aa with tr a => fun _ => f a end Pt). -Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A). Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) (P : Type) `{Pc : X -> Contr P} (g : X -> P) (h : P -> Y) (p : h o g == f) diff --git a/test-suite/bugs/closed/4292.v b/test-suite/bugs/closed/4292.v new file mode 100644 index 000000000..403e155ea --- /dev/null +++ b/test-suite/bugs/closed/4292.v @@ -0,0 +1,7 @@ +Module Type S. End S. + +Declare Module M : S. + +Module Type F (T: S). End F. + +Fail Module Type N := F with Module T := M. diff --git a/test-suite/bugs/closed/4538.v b/test-suite/bugs/closed/4538.v new file mode 100644 index 000000000..f925aae9e --- /dev/null +++ b/test-suite/bugs/closed/4538.v @@ -0,0 +1 @@ +Reserved Notation " (u *) ". diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index d14cc86fc..048f31ce3 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -841,7 +841,7 @@ End Truncation_Modalities. Module Import TrM := Modalities_Theory Truncation_Modalities. -Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition merely (A : Type@{i}) : hProp := BuildhProp (Trunc -1 A). Notation IsSurjection := (IsConnMap -1). diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v new file mode 100644 index 000000000..2c643ea77 --- /dev/null +++ b/test-suite/bugs/closed/4576.v @@ -0,0 +1,3 @@ +Definition foo := O. +Arguments foo : simpl nomatch. +Timeout 1 Eval cbn in id foo. diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v new file mode 100644 index 000000000..c862f8206 --- /dev/null +++ b/test-suite/bugs/closed/4616.v @@ -0,0 +1,4 @@ +Set Primitive Projections. +Record Foo' := Foo { foo : Type }. +Axiom f : forall t : Foo', foo t. +Extraction f. diff --git a/test-suite/bugs/closed/4663.v b/test-suite/bugs/closed/4663.v new file mode 100644 index 000000000..b76619882 --- /dev/null +++ b/test-suite/bugs/closed/4663.v @@ -0,0 +1,3 @@ +Coercion foo (n : nat) : Set. +Admitted. +Check (0 : Set). diff --git a/test-suite/bugs/closed/4670.v b/test-suite/bugs/closed/4670.v new file mode 100644 index 000000000..611399295 --- /dev/null +++ b/test-suite/bugs/closed/4670.v @@ -0,0 +1,7 @@ +Require Import Coq.Vectors.Vector. +Module Bar. + Definition foo A n (l : Vector.t A n) : True. + Proof. + induction l ; exact I. + Defined. +End Bar. diff --git a/test-suite/bugs/closed/4695.v b/test-suite/bugs/closed/4695.v new file mode 100644 index 000000000..a42271811 --- /dev/null +++ b/test-suite/bugs/closed/4695.v @@ -0,0 +1,38 @@ +(* +The Qed at the end of this file was slow in 8.5 and 8.5pl1 because the kernel +term comparison after evaluation was done on constants according to their user +names. The conversion still succeeded because delta applied, but was much +slower than with a canonical names comparison. +*) + +Module Mod0. + + Fixpoint rec_ t d : nat := + match d with + | O => O + | S d' => + match t with + | true => rec_ t d' + | false => rec_ t d' + end + end. + + Definition depth := 1000. + + Definition rec t := rec_ t depth. + +End Mod0. + + +Module Mod1. + Module M := Mod0. +End Mod1. + + +Axiom rec_prop : forall t d n, Mod1.M.rec_ t d = n. + +Lemma slow_qed : forall t n, + Mod0.rec t = n. +Proof. + intros; unfold Mod0.rec; apply rec_prop. +Timeout 2 Qed. diff --git a/test-suite/output/Intuition.out b/test-suite/output/Intuition.out index e99d9fdeb..f2bf25ca6 100644 --- a/test-suite/output/Intuition.out +++ b/test-suite/output/Intuition.out @@ -3,4 +3,4 @@ m, n : Z H : (m >= n)%Z ============================ - (m >= m)%Z + (m >= m)%Z diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index f0d2562e0..c142d28eb 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -2,40 +2,40 @@ x3 : nat ============================ - forall x x1 x4 x0 : nat, - (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal x3, x, x1, x4, x0 : nat H : forall x x3 : nat, x + x1 = x4 + x3 ============================ - x + x1 = x4 + x0 + x + x1 = x4 + x0 1 subgoal x3 : nat ============================ - forall x x1 x4 x0 : nat, - (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> - x + x1 = x4 + x0 -> foo (S x) + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> + x + x1 = x4 + x0 -> foo (S x) 1 subgoal x3 : nat ============================ - forall x x1 x4 x0 : nat, - (forall x2 x5 : nat, - x2 + x1 = x4 + x5 -> - forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> - x + x1 = x4 + x0 -> - forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x + forall x x1 x4 x0 : nat, + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, x, x1, x4, x0 : nat ============================ - (forall x2 x5 : nat, - x2 + x1 = x4 + x5 -> - forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> - x + x1 = x4 + x0 -> - forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> + x + x1 = x4 + x0 -> + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, x, x1, x4, x0 : nat @@ -44,7 +44,7 @@ forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1) H0 : x + x1 = x4 + x0 ============================ - forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x + forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, x, x1, x4, x0 : nat @@ -54,10 +54,10 @@ H0 : x + x1 = x4 + x0 x5, x6, x7, S : nat ============================ - x5 + S = x6 + x7 + Datatypes.S x + x5 + S = x6 + x7 + Datatypes.S x 1 subgoal x3, a : nat H : a = 0 -> forall a : nat, a = 0 ============================ - a = 0 + a = 0 diff --git a/test-suite/output/Quote.out b/test-suite/output/Quote.out index ca7fc3624..998eb37cc 100644 --- a/test-suite/output/Quote.out +++ b/test-suite/output/Quote.out @@ -8,17 +8,17 @@ H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ B ============================ - interp_f - (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) - (f_and (f_atom (Left_idx End_idx)) - (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) - (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) + interp_f + (Node_vm B (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (Empty_vm Prop)) + (f_and (f_atom (Left_idx End_idx)) + (f_and (f_or (f_atom End_idx) (f_atom (Left_idx End_idx))) + (f_or (f_atom (Left_idx End_idx)) (f_not (f_atom End_idx))))) 1 subgoal H : interp_f (Node_vm A (Empty_vm Prop) (Empty_vm Prop)) (f_atom End_idx) \/ B ============================ - interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) - (f_and (f_const A) - (f_and (f_or (f_atom End_idx) (f_const A)) - (f_or (f_const A) (f_not (f_atom End_idx))))) + interp_f (Node_vm B (Empty_vm Prop) (Empty_vm Prop)) + (f_and (f_const A) + (f_and (f_or (f_atom End_idx) (f_const A)) + (f_or (f_const A) (f_not (f_atom End_idx))))) diff --git a/test-suite/output/set.out b/test-suite/output/set.out index 4dfd2bc22..4b72d73eb 100644 --- a/test-suite/output/set.out +++ b/test-suite/output/set.out @@ -3,16 +3,16 @@ y1 := 0 : nat x := 0 + 0 : nat ============================ - x = x + x = x 1 subgoal y1, y2 := 0 : nat x := y2 + 0 : nat ============================ - x = x + x = x 1 subgoal y1, y2, y3 := 0 : nat x := y2 + y3 : nat ============================ - x = x + x = x diff --git a/test-suite/output/simpl.out b/test-suite/output/simpl.out index 73888da9a..526e468f5 100644 --- a/test-suite/output/simpl.out +++ b/test-suite/output/simpl.out @@ -2,14 +2,14 @@ x : nat ============================ - x = S x + x = S x 1 subgoal x : nat ============================ - 0 + x = S x + 0 + x = S x 1 subgoal x : nat ============================ - x = 1 + x + x = 1 + x diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out new file mode 100644 index 000000000..209b2bc26 --- /dev/null +++ b/test-suite/output/subst.out @@ -0,0 +1,97 @@ +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : 0 = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + x, y : nat + Hx : x = 0 + Hy : y = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : y = 3 + HB : True + H4 : 0 = 4 + ============================ + True +1 subgoal + + HA, HB : True + H4 : 0 = 4 + H3 : 0 = 3 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v new file mode 100644 index 000000000..e48aa6bb2 --- /dev/null +++ b/test-suite/output/subst.v @@ -0,0 +1,48 @@ +(* Ensure order of hypotheses is respected after "subst" *) + +Set Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *) +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + +Unset Regular Subst Tactic. +Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True. +intros * Hx Hy Hz H1 HA H2 H3 HB H4. +subst x. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *) +Show. +Undo. +subst y. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *) +Show. +Undo. +subst z. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *) +Show. +Undo. +subst. +(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *) +(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *) +Show. +trivial. +Qed. + + diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 5c60966f2..e46a556a9 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -58,22 +58,6 @@ Tactic Notation "esplit" := esplit. Global Set Regular Subst Tactic. -(** Some names have changed in the standard library, so we add aliases. *) -Require Coq.ZArith.Int. -Module Export Coq. - Module Export ZArith. - Module Int. - Module Z_as_Int. - Include Coq.ZArith.Int.Z_as_Int. - (* FIXME: Should these get a (compat "8.4")? Or be moved to Z_as_Int, probably? *) - Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing). - Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing). - Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing). - End Z_as_Int. - End Int. - End ZArith. -End Coq. - (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *) Require Coq.Numbers.Natural.Peano.NPeano. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 32e13d389..72021f2e4 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -451,4 +451,8 @@ Module Z_as_Int <: Int. Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p). Proof. reflexivity. Qed. + (** Compatibility notations for Coq v8.4 *) + Notation plus := add (compat "8.4"). + Notation minus := sub (compat "8.4"). + Notation mult := mul (compat "8.4"). End Z_as_Int. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f46b90111..04182cf23 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -241,11 +241,26 @@ let compile_files () = (** Options for proof general *) let set_emacs () = + if not (Option.is_empty !toploop) then + error "Flag -emacs is incompatible with a custom toplevel loop"; Flags.print_emacs := true; Pp.make_pp_emacs (); Vernacentries.qed_display_script := false; color := `OFF +(** Options for CoqIDE *) + +let set_ideslave () = + if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible"; + toploop := Some "coqidetop"; + Flags.ide_slave := true + +(** Options for slaves *) + +let set_toploop name = + if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible"; + toploop := Some name + (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the @@ -498,7 +513,7 @@ let parse_args arglist = |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo - |"-toploop" -> toploop := Some (next ()) + |"-toploop" -> set_toploop (next ()) |"-w" -> set_warning (next ()) (* Options with zero arg *) @@ -519,7 +534,7 @@ let parse_args arglist = |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () - |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true + |"-ideslave" -> set_ideslave () |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7c1f05cd3..a041ee620 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -848,7 +848,7 @@ let make_interpretation_vars recvars allvars = (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars let check_rule_productivity l = - if List.for_all (function NonTerminal _ -> true | _ -> false) l then + if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then error "A notation must include at least one symbol."; if (match l with SProdList _ :: _ -> true | _ -> false) then error "A recursive notation must start with at least one symbol." @@ -866,8 +866,21 @@ let is_not_printable onlyparse noninjective = function else onlyparse let find_precedence lev etyps symbols = - match symbols with - | NonTerminal x :: _ -> + let first_symbol = + let rec aux = function + | Break _ :: t -> aux t + | h :: t -> h + | [] -> assert false (* rule is known to be productive *) in + aux symbols in + let last_is_terminal () = + let rec aux b = function + | Break _ :: t -> aux b t + | Terminal _ :: t -> aux true t + | _ :: t -> aux false t + | [] -> b in + aux false symbols in + match first_symbol with + | NonTerminal x -> (try match List.assoc x etyps with | ETConstr _ -> error "The level of the leftmost non-terminal cannot be changed." @@ -890,9 +903,7 @@ let find_precedence lev etyps symbols = if Option.is_empty lev then error "A left-recursive notation must have an explicit level." else [],Option.get lev) - | Terminal _ ::l when - (match List.last symbols with Terminal _ -> true |_ -> false) - -> + | Terminal _ when last_is_terminal () -> if Option.is_empty lev then ([msg_info,strbrk "Setting notation at level 0."], 0) else [],Option.get lev diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fb57e55ef..b40f61b15 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -466,8 +466,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local,p,DefinitionBody Definition) - [Some (lid,pl), (bl,t,None)] no_hook + start_proof_and_print (local,p,DefinitionBody k) + [Some (lid,pl), (bl,t,None)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None |