From a1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Nov 2014 12:27:19 +0100
Subject: Experimenting always forcing convertibility on strict implicit
 arguments in tactic unification.

---
 interp/interp.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp')

diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a0315267..d3b7077c4b 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -10,7 +10,6 @@ Dumpglob
 Syntax_def
 Smartlocate
 Reserve
-Impargs
 Implicit_quantifiers
 Constrintern
 Modintern
-- 
cgit v1.2.3