diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 0915304c39..b6c1bfa40e 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -193,10 +193,6 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) | ARef ref -> RefKey ref, None | _ -> Oth, None -let pattern_key = function - | PatCstr (_,cstr,_,_) -> RefKey (ConstructRef cstr) - | _ -> Oth - (**********************************************************************) (* Interpreting numbers (not in summary because functional objects) *) |