From 6c65822cd241ea2f5c552f8b685490aed86eecb1 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 16 Aug 2016 17:25:43 +0200 Subject: Output a break before a list only if there was an empty line (bug #4606). Moreover, this commit makes sure that an empty line after a list is always translated into a break. ("StartLevel 1" was excluded, for some reason.) It also avoids some code duplication. In particular, "stop_item ()" is defined as "reach_item_level 0", so there is no reason to handle "StartLevel 1" specially. --- tools/coqdoc/cpretty.mll | 30 +++++++----------------------- 1 file changed, 7 insertions(+), 23 deletions(-) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 9191b2acac..6cf1eaae17 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -681,7 +681,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -742,24 +742,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -769,6 +752,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -777,10 +764,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> -- cgit v1.2.3 From 8e79ac5a766e42dfbfc629087455c9bd7639402c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Aug 2016 09:33:03 +0200 Subject: infoH: output via msg_* to make the XML protocol happy --- proofs/refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458cf..ef4cfb158d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -218,7 +218,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "") + msg_notice (str (emacs_str "") ++ (hov 0 (str s)) ++ (str (emacs_str "")) ++ fnl()); tclIDTAC goal;; -- cgit v1.2.3 From 5ef642ad47de7ff465ea2d5456c387fd35409539 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 31 Jul 2016 15:49:29 +0200 Subject: Fixing CHANGES. Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. --- CHANGES | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index c74aa7234c..de9dc649cb 100644 --- a/CHANGES +++ b/CHANGES @@ -533,6 +533,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1071,9 +1074,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions -- cgit v1.2.3 From 86935e33e8f5d4fcc4b5603086d594431a002d0b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Aug 2016 17:52:12 +0200 Subject: Fixing #5001 (metas not cleaned properly in clenv_refine_in). Fixing by copying what Matthieu did for Clenvtac.clenv_refine. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e151a06583..54977dbce7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1095,7 +1095,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac -- cgit v1.2.3 From 262ad3c3ce24463094110aa011471213ac0b61c7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 18 Aug 2016 18:47:55 +0200 Subject: Fix incorrect glob data for module symbols (bug #2336). The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library. --- interp/dumpglob.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 85212b7aba..d70d30d9ec 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir -- cgit v1.2.3 From 283579ff70d324296e2b7ee2535b1187ca32e0cb Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 19 Aug 2016 07:38:25 +0200 Subject: Remove extraneous dot in error message (bug #4832). --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 819a995db1..06a9b317a2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -610,7 +610,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in -- cgit v1.2.3 From 513e194656429b6a9142a3a34095cee2c6f8ee96 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 20 Aug 2016 10:25:37 +0200 Subject: Fixing an anomaly in printing a unification error message. --- test-suite/success/Case13.v | 8 ++++++++ toplevel/himsg.ml | 1 + 2 files changed, 9 insertions(+) diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8ee..8f95484cfd 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 13a6489b9d..ae6c86c8cc 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -307,6 +307,7 @@ let rec explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e -- cgit v1.2.3