diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:03:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:03:39 +0000 |
| commit | df7ac2d3bd49c31defc5c30138a02fd66d0b8880 (patch) | |
| tree | e2e9920962e2a6897131baf0dadde7ea50c5df89 /parsing | |
| parent | b4ec47a1e1cff29d59bbd34cdb7848ce045afa09 (diff) | |
Traduction des réferences arguments de commandes non primitives
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4331 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/pptactic.ml | 20 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 1 |
2 files changed, 11 insertions, 10 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 2d6e93ba2..e8a359316 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -229,7 +229,7 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -let rec pr_raw_generic prc prlc prtac x = +let rec pr_raw_generic prc prlc prtac prref x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen rawwit_int x) @@ -237,32 +237,32 @@ let rec pr_raw_generic prc prlc prtac x = | StringArgType -> spc () ++ str "\"" ++ str (out_gen rawwit_string x) ++ str "\"" | PreIdentArgType -> pr_arg str (out_gen rawwit_pre_ident x) | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x) - | RefArgType -> pr_arg pr_reference (out_gen rawwit_ref x) + | RefArgType -> pr_arg prref (out_gen rawwit_ref x) | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc pr_reference) + pr_arg (pr_may_eval prc prref) (out_gen rawwit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> pr_arg (pr_red_expr - (prc,pr_reference)) (out_gen rawwit_red_expr x) + (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) | ConstrWithBindingsArgType -> pr_arg (pr_with_bindings prc prlc) (out_gen rawwit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prlc prtac prref x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prref) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_raw_generic prc prlc prtac a ++ spc () ++ - pr_raw_generic prc prlc prtac b) + (fun a b -> pr_raw_generic prc prlc prtac prref a ++ spc () ++ + pr_raw_generic prc prlc prtac prref b) x) | ExtraArgType s -> let tab = @@ -666,7 +666,7 @@ and prtac x = pr6 x in (prtac,pr0,pr_match_rule false pr_pat pr_tac) let pr_raw_extend prc prlc prtac = - pr_extend_gen pi1 (pr_raw_generic prc prlc prtac) + pr_extend_gen pi1 (pr_raw_generic prc prlc prtac pr_reference) let pr_glob_extend prc prlc prtac = pr_extend_gen pi2 (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index bd06d5e1e..5d5f62f38 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -67,6 +67,7 @@ val pr_raw_generic : (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + (Libnames.reference -> std_ppcmds) -> (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds |