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.
---
 dev/printers.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index ec362b5388..2e61cb6973 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -144,7 +144,6 @@ Program
 Coercion
 Cases
 Pretyping
-Impargs
 Unification
 Declaremods
 Library
-- 
cgit v1.2.3