From ec3efbb8b59e7d3b8e5bb9fff622ab2ad0f2146b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 24 Oct 2007 14:32:02 +0000
Subject: Fix define body bug

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

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 56398a9fa6..22b0ac68c2 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -115,7 +115,7 @@ let subtac (loc, command) =
 	VernacDefinition (defkind, (locid, id), expr, hook) -> 
 	    (match expr with
 		 ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None)
-	       | DefineBody (cbl, bl, _, c, tycon) -> 
+	       | DefineBody (cbl, bl, c, tycon) -> 
 		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
-- 
cgit v1.2.3