diff options
| author | Hugo Herbelin | 2016-09-16 15:46:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-16 15:49:36 +0200 |
| commit | e6eef565639fb3840dd235eb675ece6e4dbeb082 (patch) | |
| tree | c222c842f7fad5f30bfc195962ee6984ee723fd8 /interp | |
| parent | 1a1af4f2119715245b8d4488664a8b57f4bdce08 (diff) | |
Addressing OCaml compilation warnings.
One of them revealed a true bug.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1262864c76..1f29a2948f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function e', PatCstr (loc,cstr,patl',na') let subst_binder_type_vars l = function - | Evar_kinds.BinderType (Name id) as e -> + | Evar_kinds.BinderType (Name id) -> let id = try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in |