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
---
 contrib/interface/vtp.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'contrib/interface/vtp.ml')

diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index fe227f9958..166a0cbf63 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1549,6 +1549,9 @@ and fTACTIC_COM = function
 | CT_exact_no_check(x1) ->
    fFORMULA x1;
    fNODE "exact_no_check" 1
+| CT_vm_cast_no_check(x1) ->
+   fFORMULA x1;
+   fNODE "vm_cast_no_check" 1
 | CT_exists(x1) ->
    fSPEC_LIST x1;
    fNODE "exists" 1
-- 
cgit v1.2.3