diff options
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 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 |