From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 proofs/decl_mode.ml  | 5 +++--
 proofs/decl_mode.mli | 4 ++--
 proofs/logic.ml      | 4 ++--
 3 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index f8fc4e87..134a4d8b 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: decl_mode.ml 12422 2009-10-27 08:42:49Z corbinea $ i*)
 
 open Names
 open Term
@@ -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 77bee313..bcfd6a96 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
+(* $Id: decl_mode.mli 12422 2009-10-27 08:42:49Z corbinea $ *)
 
 open Names
 open Term
@@ -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
diff --git a/proofs/logic.ml b/proofs/logic.ml
index caf6f56b..c019d45f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *)
 
 open Pp
 open Util
@@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
-    try find_mrectype env sigma ct
+    try find_mrectype env sigma (nf_evar sigma ct)
     with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec pj c in
-- 
cgit v1.2.3