From a89d858d0aea1a35d3e57d99ac0be7c6b494b282 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 14 Oct 2002 08:43:07 +0000
Subject: Ajout "Arguments Scope" pour associer des "scopes" aux arguments
 d'une référence donnée

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3133 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/xlate.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index d8663f09d3..5060b17a8e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1908,6 +1908,8 @@ let xlate_vernac =
          coerce_ID_OPT_to_FORMULA_OPT(CT_coerce_NONE_to_ID_OPT(CT_none)))*)
    | VernacOpenScope sc -> xlate_error "TODO: open scope"
 
+   | VernacArgumentsScope _ -> xlate_error "TODO: Arguments Scope"
+
    | VernacDelimiters _ -> xlate_error "TODO: Delimiters"
 
    | VernacNotation _ -> xlate_error "TODO: Notation"
-- 
cgit v1.2.3