diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-21 22:08:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-21 22:08:57 +0000 |
| commit | 7371c43d5b065e83bbaaba584dc163cac2005802 (patch) | |
| tree | 7702539290766b97222ec508fc03148ed9d659d4 | |
| parent | f0f5d9983a055e4c0f5215ad7172023b37e946c8 (diff) | |
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
| -rw-r--r-- | tactics/equality.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index df551eb29..f5ccf4286 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 |