refined the conversion oracle

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

1 files changed, 11 insertions, 10 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c705d0287..cf123f584 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -885,15 +885,16 @@ let _ =
       optread=(fun () -> get_debug () <> Tactic_debug.DebugOff);
       optwrite=vernac_debug }
 
-let vernac_set_opacity opaq r =
-  match global_with_alias r with
-    | ConstRef sp ->
-	if opaq then set_opaque_const sp
-	else set_transparent_const sp
-    | VarRef id ->
-	if opaq then set_opaque_var id
-	else set_transparent_var id
-    | _ -> error "cannot set an inductive type or a constructor as transparent"
+let vernac_set_opacity r =
+  let set_one l r =
+    let r =
+      match global_with_alias r with
+        | ConstRef sp -> ConstKey sp
+        | VarRef id -> VarKey id
+        | _ -> error
+            "cannot set an inductive type or a constructor as transparent" in
+    set_strategy r l in
+  List.iter (fun (l,q) -> List.iter (set_one l) q) r
 
 let vernac_set_option key = function
   | StringValue s -> set_string_option_value key s
@@ -1268,7 +1269,7 @@ let interp c = match c with
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
   | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
-  | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
+  | VernacSetOpacity qidl -> vernac_set_opacity qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
   | VernacUnsetOption key -> vernac_unset_option key
   | VernacRemoveOption (key,v) -> vernac_remove_option key v