refined the conversion oracle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 26 insertions, 16 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index ef1d095e20..3233852334 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -113,7 +113,6 @@ and ct_COMMAND =
   | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT
   | CT_no_inline of ct_ID_NE_LIST
   | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE
-  | CT_opaque of ct_ID_NE_LIST
   | CT_open_scope of ct_ID
   | CT_print
   | CT_print_about of ct_ID
@@ -189,13 +188,13 @@ and ct_COMMAND =
   | CT_show_script
   | CT_show_tree
   | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT
+  | CT_strategy of ct_LEVEL_LIST
   | CT_suspend
   | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
   | CT_tactic_definition of ct_TAC_DEF_NE_LIST
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
   | CT_time of ct_COMMAND
-  | CT_transparent of ct_ID_NE_LIST
   | CT_undo of ct_INT_OPT
   | CT_unfocus
   | CT_unset_option of ct_TABLE
@@ -204,6 +203,12 @@ and ct_COMMAND =
   | CT_user_vernac of ct_ID * ct_VARG_LIST
   | CT_variable of ct_VAR * ct_BINDER_NE_LIST
   | CT_write_module of ct_ID * ct_STRING_OPT
+and ct_LEVEL_LIST =
+    CT_level_list of (ct_LEVEL * ct_ID_LIST) list
+and ct_LEVEL =
+    CT_Opaque
+  | CT_Level of ct_INT
+  | CT_Expand
 and ct_COMMAND_LIST =
     CT_command_list of ct_COMMAND * ct_COMMAND list
 and ct_COMMENT =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 76b71be425..551ad3a33b 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -393,9 +393,6 @@ and fCOMMAND = function
    fOMEGA_MODE x1 ++
    fOMEGA_FEATURE x2 ++
    fNODE "omega_flag" 2
-| CT_opaque(x1) ->
-   fID_NE_LIST x1 ++
-   fNODE "opaque" 1
 | CT_open_scope(x1) ->
    fID x1 ++
    fNODE "open_scope" 1
@@ -596,6 +593,10 @@ and fCOMMAND = function
    fTACTIC_COM x2 ++
    fDOTDOT_OPT x3 ++
    fNODE "solve" 3
+| CT_strategy(CT_level_list x1) ->
+   List.fold_left (++) (mt())
+     (List.map (fun(l,q) -> fLEVEL l ++ fID_LIST q ++ fNODE "pair"2) x1) ++
+   fNODE "strategy" (List.length x1)
 | CT_suspend -> fNODE "suspend" 0
 | CT_syntax_macro(x1, x2, x3) ->
    fID x1 ++
@@ -616,9 +617,6 @@ and fCOMMAND = function
 | CT_time(x1) ->
    fCOMMAND x1 ++
    fNODE "time" 1
-| CT_transparent(x1) ->
-   fID_NE_LIST x1 ++
-   fNODE "transparent" 1
 | CT_undo(x1) ->
    fINT_OPT x1 ++
    fNODE "undo" 1
@@ -640,6 +638,10 @@ and fCOMMAND = function
    fID x1 ++
    fSTRING_OPT x2 ++
    fNODE "write_module" 2
+and fLEVEL = function
+| CT_Opaque -> fNODE "opaque" 0
+| CT_Level n -> fINT n ++ fNODE "level" 1
+| CT_Expand -> fNODE "expand" 0
 and fCOMMAND_LIST = function
 | CT_command_list(x,l) ->
    fCOMMAND x ++
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1095228b53..b3909d3170 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1796,13 +1796,11 @@ 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 (false, id :: idl) ->
-            CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (true, id :: idl)
-            -> CT_opaque (CT_id_ne_list(loc_qualid_to_ct_ID id,
-                   List.map loc_qualid_to_ct_ID idl))
-  | VernacSetOpacity (_, []) -> xlate_error "Shouldn't occur"
+  | VernacSetOpacity l ->
+      CT_strategy(CT_level_list
+        (List.map (fun (l,q) ->
+          (level_to_ct_LEVEL l,
+           CT_id_list(List.map loc_qualid_to_ct_ID q))) l))
   | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n))
   | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt)
   | VernacShow ShowNode -> CT_show_node
@@ -2196,7 +2194,12 @@ let rec xlate_vernac =
   | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
     VernacSolveExistential (_, _)|VernacCanonical _ |
      VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _)
-    -> xlate_error "TODO: vernac";;
+    -> xlate_error "TODO: vernac"
+and level_to_ct_LEVEL = function
+    Conv_oracle.Opaque -> CT_Opaque
+  | Conv_oracle.Level n -> CT_Level (CT_int n)
+  | Conv_oracle.Expand -> CT_Expand;;
+
 
 let rec xlate_vernac_list =
  function