diff options
| author | barras | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /parsing/printer.ml | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index b1d85e53a0..2d01371a56 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -123,9 +123,9 @@ let pr_constructor env cstr = open Pattern let pr_ref_label = function (* On triche sur le contexte *) - | ConstNode sp -> pr_constant (Global.env()) (sp,[||]) - | IndNode sp -> pr_inductive (Global.env()) (sp,[||]) - | CstrNode sp -> pr_constructor (Global.env()) (sp,[||]) + | ConstNode sp -> pr_constant (Global.env()) sp + | IndNode sp -> pr_inductive (Global.env()) sp + | CstrNode sp -> pr_constructor (Global.env()) sp | VarNode id -> pr_id id let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t) |