From 7371c43d5b065e83bbaaba584dc163cac2005802 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Nov 2004 22:08:57 +0000
Subject: Expansion Case dans injection et discriminate (cf bug #829)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6335 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index df551eb29a..f5ccf42869 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -329,8 +329,11 @@ let descend_then sigma env head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let arign,_ = get_arity env indf in
-      let p = it_mkLambda_or_LetIn (lift mip.mind_nrealargs resty) arign in
+      let arsign,_ = get_arity env indf in
+      let depind = build_dependent_inductive env indf in
+      let deparsign = (Anonymous,None,depind)::arsign in
+      let p =
+	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
 	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
@@ -373,7 +376,9 @@ let construct_discriminator sigma env dirn c sort =
   let (mib,mip) = lookup_mind_specif env ind in
   let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
-  let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
+  let depind = build_dependent_inductive env indf in
+  let deparsign = (Anonymous,None,depind)::arsign in
+  let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if i = dirn then true_0 else false_0 in
-- 
cgit v1.2.3