- Utilisation d'abbréviations pour les types intervenant dans RCases

- Factorisation du procédé de transformation Cases -> RCases dans Detyping
- Rebranchement de la traduction XML pour Cases (interrompue depuis
  suppression traducteur)


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

1 files changed, 11 insertions, 4 deletions

diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 36edf519bd..86ed951061 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -47,6 +47,8 @@ type 'a bindings =
 
 type 'a with_bindings = 'a * 'a bindings
 
+type predicate_pattern = name * (loc * inductive * name list) option
+
 type rawconstr = 
   | RRef of (loc * global_reference)
   | RVar of (loc * identifier)
@@ -56,9 +58,7 @@ type rawconstr =
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list * 
-      (loc * identifier list * cases_pattern list * rawconstr) list
+  | RCases of loc * rawconstr option * tomatch_tuple * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
   | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
@@ -73,7 +73,14 @@ and rawdecl = name * rawconstr option * rawconstr
 
 and fix_recursion_order = RStructRec | RWfRec of rawconstr
 
-and fix_kind = RFix of ((int option * fix_recursion_order) array * int) | RCoFix of int
+and fix_kind =
+  | RFix of ((int option * fix_recursion_order) array * int)
+  | RCoFix of int
+
+and tomatch_tuple = (rawconstr * predicate_pattern) list
+
+and cases_clauses =
+    (loc * identifier list * cases_pattern list * rawconstr) list
 
 let cases_predicate_names tml =
   List.flatten (List.map (function