diff options
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 44685d2bbd..56ce744bc1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -15,7 +15,6 @@ open Names open Constr open EConstr open Declarations -open Globnames open Genredexpr open Pattern open Reductionops @@ -79,7 +78,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () @@ -114,10 +113,8 @@ let classify_strategy (local,_ as obj) = let disch_ref ref = match ref with - EvalConstRef c -> - let c' = Lib.discharge_con c in - if c==c' then Some ref else Some (EvalConstRef c') - | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref + EvalConstRef c -> Some ref + | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref let discharge_strategy (_,(local,obj)) = if local then None else |