Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

We’re showing branches in this repository, but you can also compare across forks.

...
  • 5 commits
  • 7 files changed
  • 0 commit comments
  • 3 contributors
Commits on Jul 14, 2012
Pierre Boutillier pirbo Restore test file induct.v where the "in |- *" is mandatory
(backport of r15585)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15621 85f007b7-540e-0410-9357-904b9bb8a0f7
e70af70
Commits on Jul 19, 2012
Pierre-Marie Pédrot ppedrot Backporting r15622: Fixing goal display when still focussing but no m…
…ore goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15626 85f007b7-540e-0410-9357-904b9bb8a0f7
bde0ef0
Pierre-Marie Pédrot ppedrot Backporting r15625:
Getting rid of the undocumented [complete] tactic, which was
redundant with [solve]. The AST node still exists in Ltac, because
this is used by the [assert ... by ...] tactical. Fixes #2847.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15627 85f007b7-540e-0410-9357-904b9bb8a0f7
5ebac0a
Commits on Jul 20, 2012
Pierre-Marie Pédrot ppedrot Backporting r15628:
Let coqtop be a little more stupid in hint answer: otherwise, that
may blow up computation time by carelessly reducing potentially huge
terms.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15629 85f007b7-540e-0410-9357-904b9bb8a0f7
1a67dd9
Commits on Jul 21, 2012
courtieu backport 15635: Slight modification to the printing of goals when in …
…emacs mode.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@15636 85f007b7-540e-0410-9357-904b9bb8a0f7
de89e82
45 ide/ideproof.ml
View
@@ -109,38 +109,39 @@ let mode_cesar (proof:GText.view) = function
proof#buffer#insert ("thesis := \n "^cur_goal^"\n");
ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
+let rec flatten = function
+| [] -> []
+| (lg, rg) :: l ->
+ let inner = flatten l in
+ List.rev_append lg inner @ rg
+
let display mode (view:GText.view) goals hints evars =
let () = view#buffer#set_text "" in
match goals with
| None -> ()
(* No proof in progress *)
- | Some { Interface.fg_goals = []; Interface.bg_goals = [] } ->
- (* A proof has been finished, but not concluded *)
- begin match evars with
- | Some evs when evs <> [] ->
+ | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
+ let bg = flatten (List.rev bg) in
+ let evars = match evars with None -> [] | Some evs -> evs in
+ begin match (bg, evars) with
+ | [], [] ->
+ view#buffer#insert "No more subgoals."
+ | [], _ :: _ ->
+ (* A proof has been finished, but not concluded *)
view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
let iter evar =
let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
view#buffer#insert msg
in
- List.iter iter evs
- | _ ->
- view#buffer#insert "No more subgoals."
+ List.iter iter evars
+ | _, _ ->
+ (* No foreground proofs, but still unfocused ones *)
+ view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
+ let iter goal =
+ let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
+ view#buffer#insert msg
+ in
+ List.iter iter bg
end
- | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
- (* No foreground proofs, but still unfocused ones *)
- view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n";
- let rec flatten = function
- | [] -> []
- | (lg, rg) :: l ->
- let inner = flatten l in
- List.rev_append lg inner @ rg
- in
- let bg = flatten (List.rev bg) in
- let iter goal =
- let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
- view#buffer#insert msg
- in
- List.iter iter bg
| Some { Interface.fg_goals = fg } ->
mode view fg hints
1  parsing/g_ltac.ml4
View
@@ -80,7 +80,6 @@ GEXTEND Gram
TacFirst l
| IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
TacSolve l
- | IDENT "complete" ; ta = tactic_expr -> TacComplete ta
| IDENT "idtac"; l = LIST0 message_token -> TacId l
| IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
l = LIST0 message_token -> TacFail (n,l)
2  parsing/pptactic.ml
View
@@ -916,7 +916,7 @@ let rec pr_tac inherited tac =
| TacSolve tl ->
str "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
- str "complete" ++ spc () ++ pr_tac (lcomplete,E) t, lcomplete
+ pr_tac (lcomplete,E) t, lcomplete
| TacId l ->
str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
| TacAtom (loc,TacAlias (_,s,l,_)) ->
13 parsing/printer.ml
View
@@ -355,6 +355,8 @@ let emacs_print_dependent_evars sigma seeds =
(* spiwack: [seeds] is for printing dependent evars in emacs mode. *)
(* spiwack: [pr_first] is true when the first goal must be singled out
and printed in its entirety. *)
+(* courtieu: in emacs mode, even less cases where the first goal is printed
+ in its entirety *)
let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
let rec print_stack a = function
| [] -> Pp.int a
@@ -396,13 +398,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
str "You can use Grab Existential Variables.")
end
- | [g],[] ->
+ | [g],[] when not !Flags.print_emacs ->
let pg = default_pr_goal { it = g ; sigma = sigma } in
v 0 (
str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
++ emacs_print_dependent_evars sigma seeds
)
- | [g],a::l ->
+ | [g],a::l when not !Flags.print_emacs ->
let pg = default_pr_goal { it = g ; sigma = sigma } in
v 0 (
str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
@@ -466,7 +468,12 @@ let pr_open_subgoals () =
| [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in
begin match bgoals with
| [] -> pr_subgoals None sigma seeds stack goals
- | _ -> str"This subproof is complete, but there are still unfocused goals." ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals
+ | _ ->
+ (* emacs mode: xml-like flag for detecting information message *)
+ str (emacs_str "<infomsg>") ++
+ str"This subproof is complete, but there are still unfocused goals."
+ ++ str (emacs_str "</infomsg>")
+ ++ fnl () ++ fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds [] bgoals
end
| _ -> pr_subgoals None sigma seeds stack goals
end
6 plugins/setoid_ring/Field_theory.v
View
@@ -201,7 +201,7 @@ Theorem rdiv2:
r1 / r2 + r3 / r4 == (r1 * r4 + r3 * r2) / (r2 * r4).
Proof.
intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
apply rmul_reg_l with (r2 * r4); trivial.
rewrite rdiv_simpl; trivial.
rewrite (ARdistr_r Rsth Reqe ARth).
@@ -223,7 +223,7 @@ assert (HH1: ~ r2 == 0) by (intros HH; case H; rewrite HH; ring).
assert (HH2: ~ r5 == 0) by (intros HH; case H; rewrite HH; ring).
assert (HH3: ~ r4 == 0) by (intros HH; case H0; rewrite HH; ring).
assert (HH4: ~ r2 * (r4 * r5) == 0)
- by complete (repeat apply field_is_integral_domain; trivial).
+ by (repeat apply field_is_integral_domain; trivial).
apply rmul_reg_l with (r2 * (r4 * r5)); trivial.
rewrite rdiv_simpl; trivial.
rewrite (ARdistr_r Rsth Reqe ARth).
@@ -295,7 +295,7 @@ Hint Resolve rdiv6 .
(r1 / r2) * (r3 / r4) == (r1 * r3) / (r2 * r4).
Proof.
intros r1 r2 r3 r4 H H0.
-assert (~ r2 * r4 == 0) by complete (apply field_is_integral_domain; trivial).
+assert (~ r2 * r4 == 0) by (apply field_is_integral_domain; trivial).
apply rmul_reg_l with (r2 * r4); trivial.
rewrite rdiv_simpl; trivial.
transitivity (r2 * (r1 / r2) * (r4 * (r3 / r4))); [ ring | idtac ].
12 test-suite/success/induct.v
View
@@ -46,21 +46,21 @@ Qed.
Goal forall x, S x = S (S x).
intros.
-induction (S _) at -2.
+induction (S _) in |- * at -2.
now_show (0=1).
Undo 2.
-induction (S _) at 1 3.
+induction (S _) in |- * at 1 3.
now_show (0=1).
Undo 2.
-induction (S _) at 1.
+induction (S _) in |- * at 1.
now_show (0=S (S x)).
Undo 2.
-induction (S _) at 2.
+induction (S _) in |- * at 2.
now_show (S x=0).
Undo 2.
-induction (S _) at 3.
+induction (S _) in |- * at 3.
now_show (S x=1).
Undo 2.
-Fail induction (S _) at 4.
+Fail induction (S _) in |- * at 4.
Abort.
10 toplevel/ide_slave.ml
View
@@ -132,13 +132,13 @@ let hyp_next_tac sigma env (id,_,ast) =
("exact "^id_s),("exact "^id_s^".\n");
("generalize "^id_s),("generalize "^id_s^".\n");
("absurd <"^id_s^">"),("absurd "^type_s^".\n")
- ] @ (if Hipattern.is_equality_type ast then [
+ ] @ [
("discriminate "^id_s),("discriminate "^id_s^".\n");
("injection "^id_s),("injection "^id_s^".\n")
- ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [
+ ] @ [
("rewrite "^id_s),("rewrite "^id_s^".\n");
("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
- ] else []) @ [
+ ] @ [
("elim "^id_s), ("elim "^id_s^".\n");
("inversion "^id_s), ("inversion "^id_s^".\n");
("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
@@ -150,11 +150,11 @@ let concl_next_tac sigma concl =
"intro";
"intros";
"intuition"
- ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [
+ ] @ [
"reflexivity";
"discriminate";
"symmetry"
- ] else []) @ [
+ ] @ [
"assumption";
"omega";
"ring";

No commit comments for this range

Something went wrong with that request. Please try again.