diff options
| author | herbelin | 2000-04-30 00:53:51 +0000 |
|---|---|---|
| committer | herbelin | 2000-04-30 00:53:51 +0000 |
| commit | e867509591c1e8fad3fd764da652deb28d293d49 (patch) | |
| tree | 020f62a4157a5b13ac8de4fcd6229f34e1971064 /parsing/printer.ml | |
| parent | de22ca2b88c8350f1f9e1e2b261c42844aea4367 (diff) | |
Suite intégration de constr_pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@393 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
| -rw-r--r-- | parsing/printer.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 3e286462e8..5fa57bd39e 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -92,11 +92,15 @@ let fprtype_env env typ = fprterm_env env (incast_type typ) let fprtype = fprtype_env (gLOB nil_sign) *) -let fprterm_env a = failwith "Fw printing not implemented" -let fprterm = failwith "Fw printing not implemented" - -let fprtype_env env typ = failwith "Fw printing not implemented" -let fprtype = failwith "Fw printing not implemented" +let fprterm_env a = + warning "Fw printing not implemented, use CCI printing 1"; prterm_env a +let fprterm a = + warning "Fw printing not implemented, use CCI printing 2"; prterm a + +let fprtype_env env typ = + warning "Fw printing not implemented, use CCI printing 3"; prtype_env env typ +let fprtype a = + warning "Fw printing not implemented, use CCI printing 4"; prtype a (* For compatibility *) let fterm0 = fprterm_env |