From dcaefd4a668617504aaf335ed346598b03a80ba1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 09:47:32 +0000
Subject: Restructuration et simplification des fonctions d'affichage, de
 détypage et d'"externalisation"; standardisation du nom des fonctions
 d'affichage

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

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 4bf81f7ae2..5d2cbd57b8 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -142,9 +142,9 @@ let db_mc_pattern_success debug =
            str "Let us execute the right-hand side part..." ++ fnl())
 
 let pp_match_pattern env = function
-  | Term c -> Term (extern_pattern env (names_of_rel_context env) c)
+  | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
   | Subterm (o,c) ->
-    Subterm (o,(extern_pattern env (names_of_rel_context env) c))
+    Subterm (o,(extern_constr_pattern (names_of_rel_context env) c))
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
-- 
cgit v1.2.3