From cc0aa41c93e33d740d60884f9cf592edfa2f5ddb Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 18 Jun 2002 23:11:48 +0000 Subject: Remove lift-global function. --- generic/proof-script.el | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/generic/proof-script.el b/generic/proof-script.el index 02ae8624..2ab738a6 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1334,14 +1334,7 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; *** Theorem dependencies *** (if proof-last-theorem-dependencies - (proof-depends-process-dependencies nam gspan)) - - ;; In Coq, we have the invariant that if we've done a save and - ;; there's a top-level declaration then it must be the - ;; associated goal. (Notice that because it's a callback it - ;; must have been approved by the theorem prover.) - (and proof-lift-global - (funcall proof-lift-global gspan))))) + (proof-depends-process-dependencies nam gspan))))) ;; CASE 3: Proof completed one step or more ago, non-save ;; command seen, no nested goals allowed. -- cgit v1.2.3