diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7d225a470..07c91c8d5 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -136,7 +136,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac let constr_of_def = function | Declarations.Undef _ -> assert false | Declarations.Def cs -> Lazyconstr.force cs - | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc) + | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque lc let build_by_tactic env typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in |