From 9bf1f84def4e7635dd5b81038e5d76ee2a77204e Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 22 May 2008 17:12:11 +0000
Subject: Strategy commands are now exported

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

(limited to 'contrib/interface')

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b3909d3170..169ec0dc22 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1796,7 +1796,7 @@ let rec xlate_vernac =
        ctf_ID_OPT_SOME (xlate_ident s))
   | VernacEndProof Admitted ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE)
-  | VernacSetOpacity l ->
+  | VernacSetOpacity (_,l) ->
       CT_strategy(CT_level_list
         (List.map (fun (l,q) ->
           (level_to_ct_LEVEL l,
-- 
cgit v1.2.3