diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /dev | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 05059bd1ba..e8dffb4376 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -113,13 +113,19 @@ let pr_obj obj = Format.print_string (Libobject.object_tag obj) let cnt = ref 0 +let cast_kind_display k = + match k with + | VMcast -> "VMcast" + | DEFAULTcast -> "DEFAULTcast" + let constr_display csr = let rec term_display c = match kind_of_term c with | Rel n -> "Rel("^(string_of_int n)^")" | Meta n -> "Meta("^(string_of_int n)^")" | Var id -> "Var("^(string_of_id id)^")" | Sort s -> "Sort("^(sort_display s)^")" - | Cast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")" + | Cast (c,k, t) -> + "Cast("^(term_display c)^","^(cast_kind_display k)^","^(term_display t)^")" | Prod (na,t,c) -> "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" | Lambda (na,t,c) -> @@ -180,7 +186,7 @@ let print_pure_constr csr = | Meta n -> print_string "Meta("; print_int n; print_string ")" | Var id -> print_string (string_of_id id) | Sort s -> sort_display s - | Cast (c,t) -> open_hovbox 1; + | Cast (c,_, t) -> open_hovbox 1; print_string "("; (term_display c); print_cut(); print_string "::"; (term_display t); print_string ")"; close_box() | Prod (Name(id),t,c) -> |