diff options
| author | herbelin | 2006-05-19 09:29:54 +0000 |
|---|---|---|
| committer | herbelin | 2006-05-19 09:29:54 +0000 |
| commit | a13575eeaf69ec3dadb9b3c6a3e365a7d8371390 (patch) | |
| tree | 888718c8fd5b200aae90be89fbd16339ac40f13d /parsing/pptactic.ml | |
| parent | a171cb800c5cd7f4faf31f3fd20922d092bfd16c (diff) | |
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index f1388ab69c..d5a94cd179 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -139,7 +139,7 @@ let rec pr_raw_generic prc prlc prtac prref x = | IdentArgType -> pr_arg pr_id (out_gen rawwit_ident x) | VarArgType -> pr_arg (pr_located pr_id) (out_gen rawwit_var x) | RefArgType -> pr_arg prref (out_gen rawwit_ref x) - | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) + | SortArgType -> pr_arg pr_rawsort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> pr_arg (pr_may_eval prc prlc prref) @@ -182,7 +182,7 @@ let rec pr_glob_generic prc prlc prtac x = | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x) | VarArgType -> pr_arg (pr_located pr_id) (out_gen globwit_var x) | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x) - | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x) + | SortArgType -> pr_arg pr_rawsort (out_gen globwit_sort x) | ConstrArgType -> pr_arg prc (out_gen globwit_constr x) | ConstrMayEvalArgType -> pr_arg (pr_may_eval prc prlc @@ -228,7 +228,7 @@ let rec pr_generic prc prlc prtac x = | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) | VarArgType -> pr_arg pr_id (out_gen wit_var x) | RefArgType -> pr_arg pr_global (out_gen wit_ref x) - | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x)) + | SortArgType -> pr_arg pr_sort (out_gen wit_sort x) | ConstrArgType -> pr_arg prc (out_gen wit_constr x) | ConstrMayEvalArgType -> pr_arg prc (out_gen wit_constr_may_eval x) |