diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 21 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 3 |
2 files changed, 12 insertions, 12 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cf123f584f..8c92329e5e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -885,16 +885,15 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -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_opacity local str = + let glob_ref r = + match global_with_alias r with + | ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in + Redexpr.set_strategy local str let vernac_set_option key = function | StringValue s -> set_string_option_value key s @@ -1269,7 +1268,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 qidl -> vernac_set_opacity qidl + | VernacSetOpacity (local,qidl) -> vernac_set_opacity local qidl | VernacSetOption (key,v) -> vernac_set_option key v | VernacUnsetOption key -> vernac_unset_option key | VernacRemoveOption (key,v) -> vernac_remove_option key v diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index fd6beb2954..cce6f9a62e 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -293,7 +293,8 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * lreference * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr - | VernacSetOpacity of (Conv_oracle.level * lreference list) list + | VernacSetOpacity of + locality_flag * (Conv_oracle.level * lreference list) list | VernacUnsetOption of Goptions.option_name | VernacSetOption of Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list |