diff options
| author | herbelin | 2001-02-07 10:07:47 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-07 10:07:47 +0000 |
| commit | ec8f65e10b38a5cad9235281d5799cad76200bbb (patch) | |
| tree | f040268f6dd57a21387a56cc1e135aff3f7975c7 | |
| parent | 12c096d156c4f33d0601bc53067a5780b898cfd4 (diff) | |
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1342 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/printer.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index ac8cc92f18..97a876133d 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -111,9 +111,6 @@ let pr_inductive env ind = gentermpr (ast_of_inductive env ind) let pr_constructor env cstr = gentermpr (ast_of_constructor env cstr) -let pr_global_reference env ref = - gentermpr (ast_of_ref (ast_of_constr false env) ref) - open Pattern let pr_ref_label = function (* On triche sur le contexte *) | ConstNode sp -> pr_constant (Global.env()) (sp,[||]) |