From f39cd683cb022d877a0d2ebd014fa0879bc6de00 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 6 Dec 2004 11:28:22 +0000
Subject: Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des
 tactiques d'appliquer une éventuelle coercion vers le but

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

(limited to 'parsing/pptactic.ml')

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3057e41a41..76c9847efd 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -272,8 +272,7 @@ let rec pr_raw_generic prc prlc prtac prref x =
       pr_arg (pr_red_expr 
         (prc,prref)) (out_gen rawwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen rawwit_casted_open_constr x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -320,8 +319,7 @@ let rec pr_glob_generic prc prlc prtac x =
       pr_arg (pr_red_expr 
         (prc,pr_or_var (pr_and_short_name pr_evaluable_reference))) (out_gen globwit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (out_gen globwit_casted_open_constr x)
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x)
   | BindingsArgType -> 
@@ -367,8 +365,7 @@ let rec pr_generic prc prlc prtac x =
   | RedExprArgType ->
       pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x)
   | TacticArgType -> pr_arg prtac (out_gen wit_tactic x)
-  | CastedOpenConstrArgType ->
-      pr_arg prc (snd (out_gen wit_casted_open_constr x))
+  | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x))
   | ConstrWithBindingsArgType -> 
       pr_arg (pr_with_bindings prc prlc) (out_gen wit_constr_with_bindings x)
   | BindingsArgType -> 
-- 
cgit v1.2.3