diff options
| author | barras | 2008-05-21 23:25:22 +0000 |
|---|---|---|
| committer | barras | 2008-05-21 23:25:22 +0000 |
| commit | 82b959a8f6025f84a39efb67985e6fe1a338b94b (patch) | |
| tree | ebc83d26eb22d50d805462e770788ea11fc221d9 /toplevel | |
| parent | d01f496105de698a3ec98657e4529501c654aaeb (diff) | |
refined the conversion oracle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 21 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 12 insertions, 11 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c705d02878..cf123f584f 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 diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 986c63c0bb..fd6beb2954 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -293,7 +293,7 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * lreference * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr - | VernacSetOpacity of opacity_flag * lreference list + | VernacSetOpacity of (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 |