From 5f5eddc1779ccb0afd022d4b54ae6405d0439488 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Jul 2008 15:25:15 +0000
Subject: Autour du parsing: - Utilisation de notations de type "abbreviation
 paramétrée" plutôt que   de notations introduisant des mots-clés, là où c'est
 possible (cela affecte   QDen, in_left/in_right, inhabited, S/P dans
 NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide
 au   lieu d'échouer sur un plus long préfixe non valide de token (permet  
 notamment de faire passer la notation de Georges "'C_ G ( A )"   sans
 invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un
 point final à certains messages d'erreur qui n'en avaient pas. - Ajout
 String.copy dans string_of_label ("trou" de mutabilité signalé   par Georges
 -- le "trou" lié aux vecteurs des noeuds App restant lui   ouvert).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Utils.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c4a20506c7..149901c7bb 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -42,8 +42,8 @@ Notation dec := sumbool_of_bool.
 
 (** Hide proofs and generates obligations when put in a term. *)
 
-Notation "'in_left'" := (@left _ _ _) : program_scope.
-Notation "'in_right'" := (@right _ _ _) : program_scope.
+Notation in_left := (@left _ _ _).
+Notation in_right := (@right _ _ _).
 
 (** Extraction directives *)
 (*
@@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
-*)
\ No newline at end of file
+*)
-- 
cgit v1.2.3