diff options
| author | herbelin | 2000-05-23 19:34:48 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-23 19:34:48 +0000 |
| commit | cfb4d4e05fe41dda9507372f31b8ced11d3f2fe4 (patch) | |
| tree | 810881af4927c99f57d736da1a0ffb58242b2c7f /parsing/termast.mli | |
| parent | 9c67aa41eae70d0491ee8187a56ba60a353735d7 (diff) | |
Réparation bug d'affichage et affichage des instanciations par des {...}
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@472 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/termast.mli')
| -rw-r--r-- | parsing/termast.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/termast.mli b/parsing/termast.mli index 064dc8c25b..e0b8069d93 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -34,6 +34,7 @@ val ast_of_inductive : inductive -> Coqast.t val print_implicits : bool ref val print_casts : bool ref val print_arguments : bool ref +val print_evar_arguments : bool ref val print_coercions : bool ref val with_casts : ('a -> 'b) -> 'a -> 'b |