From 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 22 Sep 2003 18:09:11 +0000
Subject: traducteur: affiche les commentaires a l'interieur des commandes
 extraction: pb avec les variables de section definies

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e915c9ac62..b34ae524f2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -548,17 +548,17 @@ let rec extern inctx scopes vars r =
 	  (f,args) in
       (match f with
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
-	 | RRef (loc,ref) ->
+	 | RRef (rloc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
 	     let args =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     extern_app loc inctx (implicits_of_global_out ref)
-               (Some ref,extern_reference loc vars ref)
+               (Some ref,extern_reference rloc vars ref)
 	       args
-	 | RVar (loc,id) -> (* useful for translation of inductive *)
+	 | RVar (rloc,id) -> (* useful for translation of inductive *)
 	     let args = List.map (sub_extern true scopes vars) args in
 	     extern_app loc inctx (get_temporary_implicits_out id)
-	       (None,Ident (loc,v7_to_v8_id id))
+	       (None,Ident (rloc,v7_to_v8_id id))
 	       args
 	 | _       -> 
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
-- 
cgit v1.2.3