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
---
 parsing/g_tactic.ml4 | 1 +
 parsing/pptactic.ml  | 1 +
 parsing/q_coqast.ml4 | 2 ++
 3 files changed, 4 insertions(+)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9a4995c03a..a76402e096 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -309,6 +309,7 @@ GEXTEND Gram
       | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
       | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
+      | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c
 
       | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index ebf4b5ad1c..4956345120 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -652,6 +652,7 @@ and pr_atom1 = function
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
   | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
+  | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 70bc3f6822..56dd32c555 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -271,6 +271,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
   | Tacexpr.TacExactNoCheck c ->
       <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
+  | Tacexpr.TacVmCastNoCheck c ->
+      <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply cb ->
       <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (cb,cbo) ->
-- 
cgit v1.2.3