diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 95e134ae..1d7a9428 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml,v 1.54.2.2 2004/07/16 19:30:40 herbelin Exp $ *) +(* $Id: pptactic.ml,v 1.54.2.3 2005/01/15 14:56:53 herbelin Exp $ *) open Pp open Names @@ -272,8 +272,9 @@ 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) + | OpenConstrArgType -> pr_arg prc (snd (out_gen rawwit_open_constr x)) | CastedOpenConstrArgType -> - pr_arg prc (out_gen rawwit_casted_open_constr x) + pr_arg prc (snd (out_gen rawwit_casted_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) | BindingsArgType -> @@ -320,8 +321,9 @@ 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) + | OpenConstrArgType -> pr_arg prc (snd (out_gen globwit_open_constr x)) | CastedOpenConstrArgType -> - pr_arg prc (out_gen globwit_casted_open_constr x) + pr_arg prc (snd (out_gen globwit_casted_open_constr x)) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen globwit_constr_with_bindings x) | BindingsArgType -> @@ -367,6 +369,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) + | OpenConstrArgType -> pr_arg prc (snd (out_gen wit_open_constr x)) | CastedOpenConstrArgType -> pr_arg prc (snd (out_gen wit_casted_open_constr x)) | ConstrWithBindingsArgType -> |