From f93f073df630bb46ddd07802026c0326dc72dafd Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:55:59 +0000 Subject: Notation: a new annotation "compat 8.x" extending "only parsing" Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/Compare.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'theories/Arith') diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index c9e6d3cf3..d0075d741 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -10,8 +10,6 @@ Open Local Scope nat_scope. -Notation not_eq_sym := sym_not_eq. - Implicit Types m n p q : nat. Require Import Arith_base. -- cgit v1.2.3