diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-20 13:50:08 +0000 |
| commit | 9c6487ba87f448daa28158c6e916e3d932c50645 (patch) | |
| tree | 31bc965d5d14b34d4ab501cbd2350d1de44750c5 /proofs | |
| parent | 1457d6a431755627e3b52eaf74ddd09c641a9fe3 (diff) | |
COMMITED BYTECODE COMPILER
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 1 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 3 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 1 |
3 files changed, 4 insertions, 1 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 07c3aca83..e653345da 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 2e6946f72..671fbd34c 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 3e925d460..12fa2b950 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 |