From d434ab34709e0ce40f049d709332800d9a96bcc5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Apr 2003 10:35:30 +0000
Subject: Réorganisation de Impargs + mise en place d'une infrastructure
 (notatemment des tables de parsing et d'affichage différenciées) permettant
 au traducteur de changer les implicites

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 6a4de103b0..a094e17ab8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -225,9 +225,14 @@ let rec extern inctx scopes vars r =
 	 | RRef (loc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args = extern_args (extern true) scopes vars args subscopes in
-	     extern_app loc (implicits_of_global ref)
+	     extern_app loc (implicits_of_global_out ref)
                (extern_reference loc vars ref)
 	       args
+	 | RVar (loc,id) -> (* useful for translation of inductive *)
+	     let args = List.map (extern true scopes vars) args in
+	     extern_app loc (implicits_of_global_out (VarRef id))
+	       (Ident (loc,id))
+	       args
 	 | _       -> 
 	     explicitize loc [] (extern inctx scopes vars f)
                (List.map (extern true scopes vars) args))
-- 
cgit v1.2.3