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
---
 proofs/tacexpr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index d7a9879be7..b072e7cc3f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -121,6 +121,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacAssumption
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
+  | TacVmCastNoCheck of 'constr
   | TacApply of 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
-- 
cgit v1.2.3