Remove some dead code in tacinterp.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17087 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 9 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1ad8b0505..a2c461731 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -953,15 +953,6 @@ let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
 
 let adjust (l, lc) = (l, Id.Map.map (fun c -> [], c) lc)
 
-
-(* spiwack: a small wrapper around the [Matching] module *)
-
-type 'a _matching_result =
-    { s_sub : bound_ident_map * patvar_map ;
-      s_ctx : 'a ;
-      s_nxt : 'a matching_result }
-and 'a matching_result = 'a _matching_result Proofview.glist Proofview.tactic
-
 type 'a _extended_matching_result =
     { e_ctx : 'a;
       e_sub : bound_ident_map * extended_patvar_map; }