From 6725bbe3fa7a20941b4ff84c67d7cda7e7988be6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Apr 2003 15:58:14 +0000
Subject: Mécanisme plus simple et efficace pour traduire les implicites

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3889 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp/constrextern.mli')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b2dd833aaf..cb58ca58ee 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -61,3 +61,7 @@ val without_symbols : ('a -> 'b) -> 'a -> 'b
 
 (* This prints metas as anonymous holes *)
 val with_meta_as_hole : ('a -> 'b) -> 'a -> 'b
+
+(* For v8 translation *)
+val set_temporary_implicits_out :
+  (identifier * Impargs.implicits_list) list -> unit
-- 
cgit v1.2.3