From 38241e3cad7f2b5b1e2ed18fd78ba7d18dcc4f67 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 29 Apr 2008 19:07:00 +0000 Subject: Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la syntaxe interne de ring_lookup et field_lookup qui n'était pas assez robuste pour supporter une syntaxe [ ... ] dans constr. Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]" au niveau 0. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10872 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 4 +++- contrib/ring/Ring_normalize.v | 2 +- contrib/romega/ReflOmegaCore.v | 2 +- contrib/setoid_ring/Field_tac.v | 24 ++++++++++++------------ contrib/setoid_ring/Ring_tac.v | 24 ++++++++++++------------ contrib/setoid_ring/Ring_theory.v | 2 -- contrib/setoid_ring/newring.ml4 | 10 ++++------ parsing/g_ltac.ml4 | 1 + parsing/g_tactic.ml4 | 9 +++++---- theories/Init/Notations.v | 2 ++ theories/Init/Tactics.v | 3 +++ theories/Lists/List.v | 22 ++++++++++++---------- 12 files changed, 56 insertions(+), 49 deletions(-) diff --git a/CHANGES b/CHANGES index bf11db468..2fd30d416 100644 --- a/CHANGES +++ b/CHANGES @@ -63,6 +63,7 @@ Libraries (DOC TO CHECK) elements, nothing more). - In ListSet, a few definitions are now in Type (may induce a few incompatibilities). +- Notation [t;...;u] for lists made available in list_scope. - Changes in FSets/FMaps: - Improvements: in particular FMap now provides an induction principle on maps, and some properties about FSets and fold needs less hypotheses. @@ -99,7 +100,8 @@ Notations, coercions and implicit arguments (DOC TODO?) - New options Global and Local to "Implicit Arguments" for section surviving or non export outside module. -- Level "constr" moved from 9 to 8. (DOC TODO?) +- Level "constr" moved from 9 to 8 and notation "[ _ ]" now at level 0 + (easy to fix in case of incompatibilites). (DOC TODO?) - Structure/Record now printed as Record (unless option Printing All is set). - Support for parametric notations defining constants. - Insertion of coercions below product types refrains to unfold diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 4f2426337..bb3cfc5a8 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -897,6 +897,6 @@ End rings. Infix "+" := Pplus : ring_scope. Infix "*" := Pmult : ring_scope. Notation "- x" := (Popp x) : ring_scope. -Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope. +Notation "[ x ]" := (Pvar x) : ring_scope. Delimit Scope ring_scope with ring. diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 46512aab0..31ca8f804 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -879,7 +879,7 @@ Infix "+" := Tplus : romega_scope. Infix "*" := Tmult : romega_scope. Infix "-" := Tminus : romega_scope. Notation "- x" := (Topp x) : romega_scope. -Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope. +Notation "[ x ]" := (Tvar x) : romega_scope. (* \subsubsection{Definition of reified goals} *) diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v index fc89022fd..cccee6045 100644 --- a/contrib/setoid_ring/Field_tac.v +++ b/contrib/setoid_ring/Field_tac.v @@ -143,12 +143,12 @@ Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H). Tactic Notation (at level 0) "field_simplify" constr_list(rl) := let G := Get_goal in - field_lookup Field_simplify [] rl [G]. + field_lookup Field_simplify [] rl G. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in - field_lookup Field_simplify [lH] rl [G]. + field_lookup Field_simplify [lH] rl G. Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= let G := Get_goal in @@ -156,7 +156,7 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):= let g := fresh "goal" in set (g:= G); generalize H;clear H; - field_lookup Field_simplify [] rl [t]; + field_lookup Field_simplify [] rl t; intro H; unfold g;clear g. @@ -167,7 +167,7 @@ Tactic Notation "field_simplify" let g := fresh "goal" in set (g:= G); generalize H;clear H; - field_lookup Field_simplify [lH] rl [t]; + field_lookup Field_simplify [lH] rl t; intro H; unfold g;clear g. @@ -178,12 +178,12 @@ Ltac Field_simplify_in hyp:= Tactic Notation (at level 0) "field_simplify" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [] rl [t]. + field_lookup (Field_simplify_in h) [] rl t. Tactic Notation (at level 0) "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) := let t := type of h in - field_lookup (Field_simplify_in h) [lH] rl [t]. + field_lookup (Field_simplify_in h) [lH] rl t. *) (** Generic tactic for solving equations *) @@ -242,11 +242,11 @@ Ltac FIELD := Tactic Notation (at level 0) "field" := let G := Get_goal in - field_lookup FIELD [] [G]. + field_lookup FIELD [] G. Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" := let G := Get_goal in - field_lookup FIELD [lH] [G]. + field_lookup FIELD [lH] G. (* transforms a field equation to an equivalent (simplified) ring equation, and leaves non-zero conditions to be proved (field_simplify_eq) *) @@ -260,11 +260,11 @@ Ltac FIELD_SIMPL := Tactic Notation (at level 0) "field_simplify_eq" := let G := Get_goal in - field_lookup FIELD_SIMPL [] [G]. + field_lookup FIELD_SIMPL [] G. Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" := let G := Get_goal in - field_lookup FIELD_SIMPL [lH] [G]. + field_lookup FIELD_SIMPL [lH] G. (* Same as FIELD_SIMPL but in hypothesis *) @@ -323,7 +323,7 @@ Ltac FIELD_SIMPL_EQ := Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [] [t]; + field_lookup FIELD_SIMPL_EQ [] t; [ try exact I | clear H;intro H]. @@ -332,7 +332,7 @@ Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" "in" hyp(H) := let t := type of H in generalize H; - field_lookup FIELD_SIMPL_EQ [lH] [t]; + field_lookup FIELD_SIMPL_EQ [lH] t; [ try exact I |clear H;intro H]. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index d5fc5f348..46d106d37 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -250,11 +250,11 @@ Ltac Get_goal := match goal with [|- ?G] => G end. Tactic Notation (at level 0) "ring" := let G := Get_goal in - ring_lookup Ring_gen [] [G]. + ring_lookup Ring_gen [] G. Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" := let G := Get_goal in - ring_lookup Ring_gen [lH] [G]. + ring_lookup Ring_gen [lH] G. (* Simplification *) @@ -281,12 +281,12 @@ Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H). Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := let G := Get_goal in - ring_lookup Ring_simplify [] rl [G]. + ring_lookup Ring_simplify [] rl G. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := let G := Get_goal in - ring_lookup Ring_simplify [lH] rl [G]. + ring_lookup Ring_simplify [lH] rl G. (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *) @@ -296,7 +296,7 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):= let g := fresh "goal" in set (g:= G); generalize H;clear H; - ring_lookup Ring_simplify [] rl [t]; + ring_lookup Ring_simplify [] rl t; intro H; unfold g;clear g. @@ -307,13 +307,13 @@ Tactic Notation let g := fresh "goal" in set (g:= G); generalize H;clear H; - ring_lookup Ring_simplify [lH] rl [t]; + ring_lookup Ring_simplify [lH] rl t; intro H; unfold g;clear g. -(* LE RESTE MARCHE PAS DOMAGE ..... *) +(* LE RESTE MARCHE PAS DOMMAGE ..... *) @@ -343,11 +343,11 @@ Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp). Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end. Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := - match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end. + match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end. Tactic Notation (at level 0) "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= @@ -357,7 +357,7 @@ Tactic Notation (at level 0) pre(); Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [lH] rl [t]. + [lH] rl t. (* ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *) Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp). @@ -370,7 +370,7 @@ Tactic Notation (at level 0) pre(); Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] rl [t]. + [] rl t. Ltac rw_in H Heq := rewrite Heq in H. @@ -381,7 +381,7 @@ Ltac simpl_in H := pre(); Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; post()) - [] [t]. + [] t. *) diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 4c542ffdd..b7876130a 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -19,8 +19,6 @@ Reserved Notation "x -! y" (at level 50, left associativity). Reserved Notation "x *! y" (at level 40, left associativity). Reserved Notation "-! x" (at level 35, right associativity). -Reserved Notation "[ x ]" (at level 1, no associativity). - Reserved Notation "x ?== y" (at level 70, no associativity). Reserved Notation "x -- y" (at level 50, left associativity). Reserved Notation "x ** y" (at level 40, left associativity). diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index c80b37d91..c3caa403e 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -828,9 +828,8 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = lemma1;lemma2;pretac;posttac;lH;rl])) gl TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) - "[" constr(t) "]" ] -> - [ring_lookup (fst f) lH lr t] +| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> + [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t] END @@ -1163,7 +1162,6 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) - "[" constr(t) "]" ] -> - [ field_lookup (fst f) lH l t ] +| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> + [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ] END diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c541b5a7e..f7a538720 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -152,6 +152,7 @@ GEXTEND Gram tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,true,id) | n = integer -> Integer n + | r = reference -> Reference r | "()" -> TacVoid ] ] ; match_key: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 7803cd076..d59a46d12 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -244,6 +244,9 @@ GEXTEND Gram ExplicitBindings bl | bl = LIST1 constr -> ImplicitBindings bl ] ] ; + opt_bindings: + [ [ bl = bindings -> bl | -> NoBindings ] ] + ; constr_with_bindings: [ [ c = constr; l = with_bindings -> (c, l) ] ] ; @@ -527,10 +530,8 @@ GEXTEND Gram | IDENT "eright"; bl = with_bindings -> TacRight (true,bl) | IDENT "split"; bl = with_bindings -> TacSplit (false,false,bl) | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl) - | "exists"; bl = bindings -> TacSplit (false,true,bl) - | "eexists"; bl = bindings -> TacSplit (true,true,bl) - | "exists" (* meaningless? *) -> TacSplit (false,true,NoBindings) - | "eexists" -> TacSplit (true,true,NoBindings) + | "exists"; bl = opt_bindings -> TacSplit (false,true,bl) + | IDENT "eexists"; bl = opt_bindings -> TacSplit (true,true,bl) | IDENT "constructor"; n = num_or_meta; l = with_bindings -> TacConstructor (false,n,l) | IDENT "econstructor"; n = num_or_meta; l = with_bindings -> diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 9a0406d59..0aee1d4ca 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -71,6 +71,8 @@ Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). +Reserved Notation "[ x ]" (at level 0). + Delimit Scope type_scope with type. Delimit Scope core_scope with core. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index d822a45c5..602b11900 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -152,3 +152,6 @@ match goal with | _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split] | _ => fail 1 "Cannot solve this goal" end. + +(** A tactic to document or check what is proved at some point of a script *) +Ltac now_show c := change c. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 51d3f192d..2cce009a2 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,12 +1,12 @@ - (************************************************************************) - (* v * The Coq Proof Assistant / The Coq Development Team *) - (*