From a9fd21ac2b2e3908d8eb8d5a549c43949cddc69a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Nov 2014 22:30:58 +0100
Subject: Reverting the following block of three commits: - Registering strict
 implicit arguments systematically (35fc7d728168) - Experimenting always
 forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) -
 Fixing Coq compilation (894a3d16471)

Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
---
 interp/interp.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp')

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