From 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 2 Nov 2005 22:12:16 +0000
Subject: Types inductifs parametriques

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

(limited to 'contrib/cc')

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d685051e96..71545d966e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -58,7 +58,7 @@ let rec decompose_term env t=
 	let targs=Array.map (decompose_term env) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Construct c->
-	let (_,oib)=Global.lookup_inductive (fst c) in
+	let (oib,_)=Global.lookup_inductive (fst c) in
 	let nargs=mis_constructor_nargs_env env c in
 	  Constructor {ci_constr=c;
 		       ci_arity=nargs;
-- 
cgit v1.2.3