diff options
| author | herbelin | 2004-12-06 11:28:22 +0000 |
|---|---|---|
| committer | herbelin | 2004-12-06 11:28:22 +0000 |
| commit | f39cd683cb022d877a0d2ebd014fa0879bc6de00 (patch) | |
| tree | 1c691cb8f07513c905045b7b70d52872ed5e69dc /parsing/pptactic.ml | |
| parent | c81e081287075310f78081728d4a6359f6ff017a (diff) | |
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
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 9 |
1 files changed, 3 insertions, 6 deletions
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 -> |