From 063ea7f22ce7749f0b1d0c62fa37d2450356e7fd Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 30 Jan 2018 16:12:23 -0500 Subject: Delete duplicate line --- plugins/funind/indfun_common.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5a9248d47..d6fd2f2a0 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -190,7 +190,6 @@ let with_full_print f a = Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; - Impargs.make_contextual_implicit_args false; Dumpglob.pause (); try let res = f a in -- cgit v1.2.3