diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-19 20:34:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-19 20:34:59 +0200 |
| commit | 82dc377451e2dc7810eea136b9a6ab8fc5ae48b5 (patch) | |
| tree | 19336aad14e3e1c40dd8ee88f058d8d518e1c42f /library/impargs.ml | |
| parent | 05f3192fedc354eb34ac10813bd7f1ffadfd4405 (diff) | |
Removing dead code in Impargs.
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e2110..db98bb9fd 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicits f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt |