diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 907cd474c4..011aba5d7d 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -798,8 +798,8 @@ let ltac_ring_structure e = open Proofview.Notations let ring_lookup (f:glob_tactic_expr) lH rl t = - Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> + Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> let rl = make_args_list rl t in let e = find_ring_structure env sigma rl in let rl = carg (make_term_list e.ring_carrier rl) in @@ -1119,8 +1119,8 @@ let ltac_field_structure e = field_simpl_eq_in_ok;cond_ok;pretac;posttac] let field_lookup (f:glob_tactic_expr) lH rl t = - Goal.env >>- fun env -> - Goal.defs >>- fun sigma -> + Proofview.tclEVARMAP >= fun sigma -> + Proofview.Goal.env >>- fun env -> let rl = make_args_list rl t in let e = find_field_structure env sigma rl in let rl = carg (make_term_list e.field_carrier rl) in |