diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 10:09:34 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 10:09:34 +0000 |
| commit | bb7d7482724489521dde94a5b70af7864acfa802 (patch) | |
| tree | 821dfa6baa108de2b2af016e842164f01a39101f /dev | |
| parent | 05b756a9a5079e91c5015239bb801918d4903c08 (diff) | |
nouvelle implantation de la reduction
suppression de IsXtra du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 95c85866d..7cb08e06b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -82,7 +82,6 @@ let constr_display csr = | IsMeta n -> "Meta("^(string_of_int n)^")" | IsVar id -> "Var("^(string_of_id id)^")" | IsSort s -> "Sort("^(sort_display s)^")" - | IsXtra s -> "Xtra("^s^")" | IsCast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")" | IsProd (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" @@ -145,7 +144,6 @@ let print_pure_constr csr = | IsMeta n -> print_string "Meta("; print_int n; print_string ")" | IsVar id -> print_string (string_of_id id) | IsSort s -> sort_display s - | IsXtra s -> print_string ("Xtra("^s^")") | IsCast (c,t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() |