diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-12 12:27:25 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-12 12:27:25 +0000 |
| commit | 7248f6cccfcca2b0d59b244e8789590794aefc45 (patch) | |
| tree | 8979753245e2ff2ef183d37ba324f64c90b5d337 /theories/Classes/SetoidTactics.v | |
| parent | bba897d5fd964bef0aa10102ef41cee1ac5fc3bb (diff) | |
- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to
change the default pretty-printing to use Π, λ instead of
forall and fun (and allow "," as well as "=>" for "fun" to be more
consistent with the standard forall and exists syntax). Parsing allows
theses new forms too, even if not in -unicode, and does not make Π or
λ keywords. As usual, criticism and suggestions are welcome :)
Not sure what to do about "->"/"→" ?
- [setoid_replace by] now uses tactic3() to get the right parsing level
for tactics.
- Type class [Instance] names are now mandatory.
- Document [rewrite at/by] and fix parsing of occs to support their
combination.
- Backtrack on [Enriching] modifier, now used exclusively in the
implementation of implicit arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index aeaa197e8..aea6f5d7a 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -76,23 +76,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) setoidreplaceinat (default_relation x y) id idtac o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) - "by" tactic(t) := + "by" tactic3(t) := setoidreplace (default_relation x y) ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) - "by" tactic(t) := + "by" tactic3(t) := setoidreplaceat (default_relation x y) ltac:t o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) - "by" tactic(t) := + "by" tactic3(t) := setoidreplacein (default_relation x y) id ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) - "by" tactic(t) := + "by" tactic3(t) := setoidreplaceinat (default_relation x y) id ltac:t o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) @@ -106,13 +106,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) - "by" tactic(t) := + "by" tactic3(t) := setoidreplace (rel x y) ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) - "by" tactic(t) := + "by" tactic3(t) := setoidreplaceat (rel x y) ltac:t o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) @@ -129,14 +129,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) - "by" tactic(t) := + "by" tactic3(t) := setoidreplacein (rel x y) id ltac:t. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) - "by" tactic(t) := + "by" tactic3(t) := setoidreplaceinat (rel x y) id ltac:t o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back |