From 9c6487ba87f448daa28158c6e916e3d932c50645 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 20 Oct 2004 13:50:08 +0000
Subject: COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenvtac.ml | 1 +
 proofs/pfedit.ml   | 3 ++-
 proofs/tacexpr.ml  | 1 +
 3 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 07c3aca835..e653345dad 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -22,6 +22,7 @@ open Proof_type
 open Refiner
 open Proof_trees
 open Logic
+open Reduction
 open Reductionops
 open Tacmach
 open Evar_refiner
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2e6946f721..671fbd34c7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -192,7 +192,8 @@ let cook_proof () =
   (ident,
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
-      const_entry_opaque = true },
+      const_entry_opaque = true;
+      const_entry_boxed = false},
     strength, ts.top_hook))
 
 let current_proof_statement () = 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3e925d4609..12fa2b950a 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -113,6 +113,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacIntroMove of identifier option * identifier located option
   | TacAssumption
   | TacExact of 'constr
+  | TacExactNoCheck of 'constr
   | TacApply of 'constr with_bindings
   | TacElim of 'constr with_bindings * 'constr with_bindings option
   | TacElimType of 'constr
-- 
cgit v1.2.3