diff options
| author | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
| commit | 8500216ac8df90b2afc0f5fd42d714cc87c6bde6 (patch) | |
| tree | 76a1ebe10646d2432f1539fb7ee9c6b0691ea221 /plugins/setoid_ring | |
| parent | 9281bb33f2b9aa5d762f8b5b8b0159984b696efb (diff) | |
| parent | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (diff) | |
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a736eec5e7..b05e1e85b7 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -99,7 +99,7 @@ let protect_tac_in map id = let rec closed_under sigma cset t = try let (gr, _) = Termops.global_of_constr sigma t in - Refset_env.mem gr cset + GlobRef.Set_env.mem gr cset with Not_found -> match EConstr.kind sigma t with | Cast(c,_,_) -> closed_under sigma cset c @@ -111,7 +111,7 @@ let closed_term args _ = match args with let t = Option.get (Value.to_constr t) in let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in Proofview.tclEVARMAP >>= fun sigma -> - let cs = List.fold_right Refset_env.add l Refset_env.empty in + let cs = List.fold_right GlobRef.Set_env.add l GlobRef.Set_env.empty in if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) | _ -> assert false |
