From 722d0c21cb2f8da64b1c54f854c8dc401edd25e6 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Tue, 27 Oct 2009 08:57:43 +0000
Subject: fixed czar bug with parametric inductives

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12423 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/decl_mode.ml  | 3 ++-
 proofs/decl_mode.mli | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index a32b9777ba..ba675327c6 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -45,7 +45,7 @@ type split_tree=
   | Split_patt of Idset.t * inductive *
 		(bool array * (Idset.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * int)
+  | End_patt of (identifier * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
@@ -124,3 +124,4 @@ let get_last env =
   try
     let (id,_,_) =  List.hd (Environ.named_context env) in id
   with Invalid_argument _ -> error "no previous statement to use"
+
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index e225c828d2..734dc04421 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -33,7 +33,7 @@ type split_tree=
   | Split_patt of Idset.t * inductive *
 		(bool array * (Idset.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * int)
+  | End_patt of (identifier * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
-- 
cgit v1.2.3