Fixing some tests from the test-suite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16760 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 8548a21b82..a771184716 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -438,9 +438,12 @@ let pr_lazy lz = if lz then str "lazy" else mt ()
 
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
-  | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]"
+  | Subterm (b,None,a) ->
+    (** ppedrot: we don't make difference between [appcontext] and [context]
+        anymore, and the interpretation is governed by a flag instead. *)
+    str "context [" ++ pr_pat a ++ str "]"
   | Subterm (b,Some id,a) ->
-      (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+    str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
 
 let pr_match_hyps pr_pat = function
   | Hyp (nal,mp) ->