From 0c4965dd44ae43fc4fdae29854584281d1cf82cc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Jul 2006 21:37:15 +0000
Subject: Ajout de quelques Arguments Scope pour simuler la récursivité du
 scope romega_scope en compensation (et anticipation) d'une suppression de la
 récursivité des délimiteurs de scope (ici %term)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9041 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/ReflOmegaCore.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 2aa3516f1d..83ea5b637e 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -49,6 +49,11 @@ Inductive term : Set :=
   | Tvar : nat -> term.
 
 Delimit Scope romega_scope with term.
+Arguments Scope Tplus [romega_scope romega_scope].
+Arguments Scope Tmult [romega_scope romega_scope].
+Arguments Scope Tminus [romega_scope romega_scope].
+Arguments Scope Topp [romega_scope romega_scope].
+
 Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
 Infix "-" := Tminus : romega_scope.
-- 
cgit v1.2.3