From c84fd703d6d00494e62b0fa5fb609cda67132133 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Wed, 25 Nov 2009 15:15:54 +0000
Subject: Fix for notation scope & inductive types

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12542 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 63f653edae..6fdfb57329 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -980,10 +980,10 @@ let add_notation_interpretation (df,c,sc) =
   add_notation_interpretation_core false df c sc false
 
 let set_notation_for_interpretation impls (df,c,sc) =
-  Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc;
-  try silently (add_notation_interpretation_core false df ~impls c sc) false;
+  (try silently (add_notation_interpretation_core false df ~impls c sc) false;
   with NoSyntaxRule ->
-    error "Parsing rule for this notation has to be previously declared."
+    error "Parsing rule for this notation has to be previously declared.");
+  Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
-- 
cgit v1.2.3