From 9e8f49b1fd4d08808a5f708e09aa51a43e4ceee7 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Thu, 14 Nov 2013 15:21:36 +0000
Subject: Remove some dead code in tacinterp.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17087 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1ad8b05053..a2c461731e 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; }
-- 
cgit v1.2.3