diff options
| author | Emilio Jesus Gallego Arias | 2018-09-18 15:22:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-06 14:32:23 +0200 |
| commit | 53870b7f6890a593d1da93706f3d020a79d226e5 (patch) | |
| tree | 0f6e1afa1ca58611e6a12596ef10c88359b8045e /proofs/redexpr.ml | |
| parent | 371566f7619aed79aad55ffed6ee0920b961be6e (diff) | |
[api] Remove (most) 8.9 deprecated objects.
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
Diffstat (limited to 'proofs/redexpr.ml')
| -rw-r--r-- | proofs/redexpr.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 1350da65dc..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) | _ -> () @@ -115,7 +114,7 @@ let classify_strategy (local,_ as obj) = let disch_ref ref = match ref with EvalConstRef c -> Some ref - | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else 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 |