From 97fb9f22eadab06fe320ccedf6abfb6be89702f4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Apr 2008 14:41:07 +0000
Subject: Ajout "simple apply" et "simple eapply" pour apply sans unfold

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10738 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 7775dc9816..aded98828e 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -672,8 +672,9 @@ and pr_atom1 = function
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
   | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
-  | TacApply (ev,cb) ->
-      hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ 
+  | TacApply (a,ev,cb) ->
+      hov 1 ((if a then str "simple " else mt()) ++
+             str (if ev then "eapply" else "apply") ++ spc () ++ 
              pr_with_bindings cb)
   | TacElim (ev,cb,cbo) ->
       hov 1 (str (if ev then "eelim" else "elim") ++ pr_arg pr_with_bindings cb ++ 
-- 
cgit v1.2.3