aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES6
-rw-r--r--interp/dumpglob.ml5
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--test-suite/success/Case13.v8
-rw-r--r--tools/coqdoc/cpretty.mll30
-rw-r--r--toplevel/himsg.ml1
7 files changed, 24 insertions, 30 deletions
diff --git a/CHANGES b/CHANGES
index 8f873bd91..17e397d6e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -626,6 +626,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").
@@ -1164,9 +1167,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
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 931fc1ca4..1e14eeb81 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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2c97cf442..3e5b7b65f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -629,7 +629,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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d08ada60..acc0fa1ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1270,7 +1270,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
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index f14725a8e..8f95484cf 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/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 005ffdae7..919f37b91 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -675,7 +675,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
}
@@ -736,24 +736,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
@@ -763,6 +746,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* _
@@ -771,10 +758,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,_) ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b3eae3765..ff4c18ad2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -320,6 +320,7 @@ let 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