diff options
| author | Emilio Jesus Gallego Arias | 2019-02-24 20:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:30:13 +0200 |
| commit | 7dc04f0244aeb277b62070f87590cbc2cafd8396 (patch) | |
| tree | a11175ee231e93c351f0a70bece257f6de840c4e /proofs | |
| parent | a296e879112f2e88b2fdfbf2fe90f1807f90b890 (diff) | |
[proof] drop parameter from terminator type
This makes the type of terminator simpler, progressing towards its
total reification.
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; |