diff options
| author | msozeau | 2008-05-12 12:27:25 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-12 12:27:25 +0000 |
| commit | 7248f6cccfcca2b0d59b244e8789590794aefc45 (patch) | |
| tree | 8979753245e2ff2ef183d37ba324f64c90b5d337 /doc/refman/Setoid.tex | |
| 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 'doc/refman/Setoid.tex')
| -rw-r--r-- | doc/refman/Setoid.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 8bdf6ab0a2..d2b6d11516 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -540,7 +540,7 @@ the prefixed tactics it is possible to pass additional arguments such as The \texttt{using relation} arguments cannot be passed to the unprefixed form. The latter argument -tells the tactic what parametric relation should be used to replace +tells the tactic what parametric relation should be used to replace the first tactic argument with the second one. If omitted, it defaults to the \texttt{DefaultRelation} instance on the type of the objects. By default, it means the most recent \texttt{Equivalence} instance in @@ -679,7 +679,7 @@ If a signature mentions a relation $R$ on the left of an arrow is smaller than $R$, and the inverse applies on the right of an arrow. One can then declare only a few morphisms instances that generate the complete set of signatures for a particular constant. By default, the only declared -subrelations is \texttt{iff}, which is a subrelation of \texttt{impl} +subrelation is \texttt{iff}, which is a subrelation of \texttt{impl} and \texttt{inverse impl} (the dual of implication). That's why we can declare only two morphisms for conjunction: \verb|Morphism (impl ==> impl ==> impl) and| and |