aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorletouzey2010-11-16 17:27:17 +0000
committerletouzey2010-11-16 17:27:17 +0000
commite216c2de60d1d8b1fd35169257349fa4c257a516 (patch)
treee3ba078fa4bb837c8708f6f8673f3438ec0e6526 /plugins/syntax/string_syntax.ml
parentb9f4f52371fef6c94a0b2de4784aefe95c793a51 (diff)
Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.
No infix notation "rem" for Zrem (that will probably become Z.rem in a close future). This way, we avoid conflict with people already using rem for their own need. Same for BigZ. We still use infix rem, but only in the abstract layer of Numbers, in a way that doesn't inpact the rest of Coq. Btw, the axiomatized function is now named rem instead of remainder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions