diff options
Diffstat (limited to 'plugins/setoid_ring/newring.ml4')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b8507041f..0cb9d4460 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -22,7 +22,6 @@ open Glob_term open Tacticals open Tacexpr open Coqlib -open Tacmach open Mod_subst open Tacinterp open Libobject @@ -797,8 +796,6 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -open Proofview.Notations - let ring_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in |