Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 7 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 161c37ae8..ca25938b6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -69,14 +69,20 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
       let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in
       let lnamesar,_ = get_arity env indf in
       let ci = make_default_case_info env RegularStyle ind in
+      let depind = build_dependent_inductive env indf in
+      let deparsign = (Anonymous,None,depind)::lnamesar in
+      let p = (* mkRel nbprod *)
       it_mkLambda_or_LetIn_name env'
-       	(lambda_create env'
-           (build_dependent_inductive env indf,
-            mkCase (ci,
-		       mkRel (nbprod+nbargsprod),
-		       mkRel 1,
-		       rel_vect nbargsprod k)))
-       	lnamesar
+          (appvect
+            (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod),
+            if dep then extended_rel_vect 0 deparsign
+            else extended_rel_vect 0 lnamesar))
+          (if dep then deparsign else lnamesar) in
+      it_mkLambda_or_LetIn_name env'
+       	(mkCase (ci, lift nbargsprod p,
+		     mkRel 1,
+		     rel_vect nbargsprod k))
+       	deparsign
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       let t = build_branch_type env dep (mkRel (k+1)) cs in