From ad31926a8a97ebf41f700feee0194b294474a791 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 7 Oct 2010 18:37:44 +0000
Subject: Fix bug# 2392

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

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index a663d3db33..fccb2f9332 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -119,7 +119,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
     match props with
     | Inr term ->
 	let c = interp_casted_constr_evars evars env' term cty in
-	  Inr (c, subst)
+	  Inr c
     | Inl props ->
 	let get_id =
 	  function
@@ -159,7 +159,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
 	let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
 	  term, termtype
-    | Inr (def, subst) ->
+    | Inr def ->
 	let termtype = it_mkProd_or_LetIn cty ctx in
 	let term = Termops.it_mkLambda_or_LetIn def ctx in
 	  term, termtype
-- 
cgit v1.2.3