From fff07f8260867740f1f8d8b09bd26baa5f99e5c6 Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Sat, 22 Jul 2006 17:42:45 +0000
Subject: - Ajout d'un cast vm dans la syntaxe :  x <: t     Part contre ces
 cas sont detruis dans les "Definition"     (pas dans les "Lemma") je
 comprends pas ou ils sont enlev'e...     Si une id'ee ...

- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.

- Meilleur compilation des coinductifs, on utilise maintenant vraimment
  du lazy. 

- Enfin un peu plus de doc dans le code de la vm.

  Benjamin



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/vm_printers.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'dev')

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index c037eca7cc..1e1144895f 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -65,8 +65,6 @@ and ppatom a =
       print_string (string_of_kn sp);
       print_string ","; print_int i;
       print_string ")"
-  | Afix_app _ -> print_vfix_app ()
-  | Aswitch _ -> print_vswith()
 
 and ppwhd whd =
   match whd with 
@@ -74,9 +72,7 @@ and ppwhd whd =
   | Vprod _ -> print_string "product"
   | Vfun _ -> print_string "function"
   | Vfix _ -> print_vfix()
-  | Vfix_app _ -> print_vfix_app()
   | Vcofix _ -> print_string "cofix"
-  | Vcofix_app _ -> print_string "cofix_app"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
   | Vconstr_block b -> ppvblock b      
   | Vatom_stk(a,s) ->
-- 
cgit v1.2.3