diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 2 |
2 files changed, 0 insertions, 5 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 96d90e9252..a871a3fc95 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -24,9 +24,6 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) -(* Extra info on proofs. *) -type lemma_possible_guards = int list list - type proof_object = { id : Names.Id.t; entries : Evd.side_effects Entries.definition_entry list; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index f84ec27df7..9c2ada2457 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -31,8 +31,6 @@ val compact_the_proof : t -> t function which takes a [proof_object] together with a [proof_end] (i.e. an proof ending command) and registers the appropriate values. *) -type lemma_possible_guards = int list list - type proof_object = { id : Names.Id.t; entries : Evd.side_effects Entries.definition_entry list; |