diff options
| author | herbelin | 2000-04-26 14:10:22 +0000 |
|---|---|---|
| committer | herbelin | 2000-04-26 14:10:22 +0000 |
| commit | 344872455282a7d00d40a8dd025996b6709b4572 (patch) | |
| tree | df14b6175208279184971564467432fb48b577f9 /parsing/printer.ml | |
| parent | b95e0780ccbab4e4d89b84f8ec92a5548f663794 (diff) | |
Introduction d'un type constr_pattern pour les différents filtrages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@371 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 99db762e02..36f8d11a36 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -97,6 +97,13 @@ let pr_existential ev = gencompr CCI (ast_of_existential ev) let pr_inductive ind = gencompr CCI (ast_of_inductive ind) let pr_constructor cstr = gencompr CCI (ast_of_constructor cstr) +open Rawterm +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,[||]) + | VarNode id -> print_id id + (* For compatibility *) let term0 = prterm_env let fterm0 = fprterm_env |