From 7dc04f0244aeb277b62070f87590cbc2cafd8396 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 24 Feb 2019 20:27:09 +0100
Subject: [proof] drop parameter from terminator type

This makes the type of terminator simpler, progressing towards its
total reification.
---
 proofs/proof_global.ml  | 3 ---
 proofs/proof_global.mli | 2 --
 2 files changed, 5 deletions(-)

(limited to 'proofs')

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;
-- 
cgit v1.2.3