diff options
| author | coq | 2001-04-23 15:07:44 +0000 |
|---|---|---|
| committer | coq | 2001-04-23 15:07:44 +0000 |
| commit | a3837fa9dd60b7b8528e2e31c98682528c694dcd (patch) | |
| tree | 9b51b3054b6844a2f346d23a199828ba49ea8097 /theories/ZArith | |
| parent | 5993237b592c726d6777608623a7cc063b1dabb9 (diff) | |
Minor layout adjustments for Library doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1672 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zsyntax.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 1981080a2b..62fd1796eb 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -78,12 +78,12 @@ Grammar constr pattern := to avoid printings like |``x` + `y`` < `45`| for |x + y < 45|. So when a Z-expression is to be printed, its sub-expresssions are - enclosed into an ast (ZEXPR \$subexpr). (ZEXPR \$s) is printed like \$s + enclosed into an ast (ZEXPR \$subexpr), which is printed like \$subexpr but without symbols "`" "`" around. - There is just one problem: NEG and Zopp have the same printing rules. - If Zopp is opaque, we may not be able to solve a goal like - ` -5 = -5 ` by reflexivity. (In fact, this precise Goal is solved + There is just one problem: NEG and Zopp have the same printing rules. + If Zopp is opaque, we may not be able to solve a goal like + ` -5 = -5 ` by reflexivity. (In fact, this precise Goal is solved by the Reflexivity tactic, but more complex problems may arise SOLUTION : Print (Zopp 5) for constants and -x for variables *) |