From 8d524ae3e9b2e2394bcfc0b47d4a8eba969161c4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 31 Mar 2006 18:21:20 +0000
Subject: Amendement impression evar pour affichage des Meta par 'info'

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fcdd0a786e..2fe967153f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -638,6 +638,8 @@ let rec extern inctx scopes vars r =
 
   | RVar (loc,id) -> CRef (Ident (loc,id))
 
+  | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
+
   | REvar (loc,n,_) -> (* we drop args *) extern_evar loc n
 
   | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
-- 
cgit v1.2.3