diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 07c91c8d5..f0ea69533 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -135,8 +135,8 @@ 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 lc + | Declarations.Def cs -> Mod_subst.force_constr cs + | Declarations.OpaqueDef lc -> Opaqueproof.force_proof lc let build_by_tactic env typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in |