From 1f84b509851f3eead190eac2300ee77611ed9ff4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Oct 2011 13:57:13 +0000
Subject: Fix bug #2557 and an issue with Propers for complement

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

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 9fc3cb59ce..000ffc6226 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -166,7 +166,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	in
 	let app, ty_constr = instance_constructor k subst in
 	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
+	let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
 	  term, termtype
     | Inr def ->
 	let termtype = it_mkProd_or_LetIn cty ctx in
-- 
cgit v1.2.3