From c86d78c0f18fb28f74bb6b192c03ebe73117cf03 Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Mon, 11 Dec 2006 18:46:35 +0000
Subject: Changement dans le kernel :    - essai de suppression des dependances
 debiles. (echec)    - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




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

(limited to 'kernel/vm.ml')

diff --git a/kernel/vm.ml b/kernel/vm.ml
index de9bd753a0..131e8320f4 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -469,8 +469,6 @@ let check_cofix vcf1 vcf2 =
   (current_cofix vcf1 = current_cofix vcf2) &&
   (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
 
-external print_point : Obj.t -> unit = "coq_print_pointer"
-
 let reduce_cofix k vcf =
   let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
   let ndef = Array.length fc_typ in
-- 
cgit v1.2.3