diff options
| author | herbelin | 2000-05-26 15:57:50 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-26 15:57:50 +0000 |
| commit | 2372cbdcabec698e5deb5abfc393ed3e6909995f (patch) | |
| tree | 57021a056665c433ca41aee125825bbeb7bc6d58 /parsing/printer.ml | |
| parent | b726fcfd1de249ab4fb5bb82f64fa349d2c17a0f (diff) | |
Modification messages d'erreurs, possibilité de n'importe quel constr dans les instances de références
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index bad9c38667..5a4f8ae5bd 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -119,16 +119,17 @@ let fprtype a = (* For compatibility *) let fterm0 = fprterm_env -let pr_constant cst = gentermpr (ast_of_constant cst) -let pr_existential ev = gentermpr (ast_of_existential ev) -let pr_inductive ind = gentermpr (ast_of_inductive ind) -let pr_constructor cstr = gentermpr (ast_of_constructor cstr) +let pr_constant env cst = gentermpr (ast_of_constant (unitize_env env) cst) +let pr_existential env ev = gentermpr (ast_of_existential (unitize_env env) ev) +let pr_inductive env ind = gentermpr (ast_of_inductive (unitize_env env) ind) +let pr_constructor env cstr = + gentermpr (ast_of_constructor (unitize_env env) cstr) open Pattern let pr_ref_label = function (* On triche sur le contexte *) - | ConstNode sp -> pr_constant (sp,[||]) - | IndNode sp -> pr_inductive (sp,[||]) - | CstrNode sp -> pr_constructor (sp,[||]) + | ConstNode sp -> pr_constant (Global.context()) (sp,[||]) + | IndNode sp -> pr_inductive (Global.context()) (sp,[||]) + | CstrNode sp -> pr_constructor (Global.context()) (sp,[||]) | VarNode id -> print_id id let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t) |