diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-05 16:50:04 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-05 16:57:45 +0100 |
| commit | 8fc2509f354b02ec4e0a3eb6fabc329109686c47 (patch) | |
| tree | bf7f0738e36d861d57029985ea4f2d3e73d23c15 /proofs/pfedit.ml | |
| parent | adfd437f8ae6aaf893119fa4730edecf067dede7 (diff) | |
Remove some dead-code (thanks to ocaml warnings)
The removed code isn't used locally and isn't exported in the signature
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index ca760c456..68c2ed328 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -25,9 +25,6 @@ let delete_proof = Proof_global.discard let delete_current_proof = Proof_global.discard_current let delete_all_proofs = Proof_global.discard_all -let set_undo _ = () -let get_undo _ = None - let start_proof (id : Id.t) str hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in Proof_global.start_proof id str goals terminator; @@ -132,11 +129,6 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac delete_current_proof (); raise reraise -let constr_of_def = function - | Declarations.Undef _ -> assert false - | 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 let sign = val_of_named_context (named_context env) in |