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, 23 insertions, 2 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a64c553899..adc5932f18 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -239,6 +239,28 @@ let find_coinductive env sigma c =
 (* find appropriate names for pattern variables. Useful in the
    Case tactic. *)
 
+let is_dep_predicate env kelim pred nodep_ar = 
+  let rec srec env pval pt nodep_ar =
+    let pt' = whd_betadeltaiota env Evd.empty pt in
+    let pv' = whd_betadeltaiota env Evd.empty pval in
+    match kind_of_term pv', kind_of_term pt', kind_of_term nodep_ar with
+      | Lambda (na,t,b), Prod (_,_,a), Prod (_,_,a') ->
+	  srec (push_rel_assum (na,t) env) b a a'
+      | _,              Prod (na,t,a), Prod (_,_,a') ->
+	  srec (push_rel_assum (na,t) env) (lift 1 pv') a a'
+      | Lambda (_,_,b), Prod (_,_,_), _ -> (*dependent (mkRel 1) b*) true
+      | _, Prod (_,_,_), _ -> true
+      | _ -> false in 
+  srec env pred.uj_val pred.uj_type nodep_ar
+
+let is_dependent_elimination_predicate env pred indf =
+  let (ind,params) = indf in
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  let kelim = mip.mind_kelim in
+  let arsign,s = get_arity env indf in
+  let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
+  is_dep_predicate env kelim pred glob_t
+
 let is_dep_arity env kelim predty nodep_ar = 
   let rec srec pt nodep_ar =
     let pt' = whd_betadeltaiota env Evd.empty pt in
@@ -256,7 +278,6 @@ let is_dependent_elimination env predty indf =
   let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in
   is_dep_arity env kelim predty glob_t
 
-
 let set_names env n brty =
   let (ctxt,cl) = decompose_prod_n_assum n brty in
   it_mkProd_or_LetIn_name env cl ctxt
@@ -277,7 +298,7 @@ let type_case_branches_with_names env indspec pj c =
   let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let params = list_firstn mip.mind_nparams args in
-  if is_dependent_elimination env pj.uj_type (ind,params) then
+  if is_dependent_elimination_predicate env pj (ind,params) then
     (set_pattern_names env ind lbrty, conclty)
   else (lbrty, conclty)