diff options
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 0 insertions, 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; } |