From 1a1ee340de86b6688a8ceeec5eaa8e76032fe3f3 Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 2 Nov 2013 15:34:09 +0000
Subject: Getting rid of Goal.here, and all the related exceptions and
 combinators.

It was a bad idea. The new API based on lists seems more sensible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/elim.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/elim.ml')

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 0e30daf6d..a784264f0 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -111,7 +111,7 @@ let head_in =
 
 let decompose_these c l =
   let indl = (*List.map inductive_of*) l in
-  head_in >>- fun head_in ->
+  Proofview.Goal.lift head_in >>- fun head_in ->
   general_decompose (fun (_,t) -> head_in indl t) c
 
 let decompose_nonrec c =
-- 
cgit v1.2.3