- Distinction explicite des parties paramètres et arguments dans le type

  des inductifs de la clause "in" du filtrage.
- Débogage et extension du parseur xml (g_xml.ml4)


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

3 files changed, 6 insertions, 15 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 1234c7faaa..681e43af0f 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -561,10 +561,8 @@ let rec build_entry_lc funnames avoid rt  : rawconstr build_entry_return =
 	build_entry_lc funnames  avoid b
     | RDynamic _ -> error "Not handled RDynamic"
 and build_entry_lc_from_case funname make_discr
-    (el:(Rawterm.rawconstr *
-	   (Names.name * (loc * Names.inductive * Names.name list) option) )
-       list)
-    (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid : 
+    (el:tomatch_tuple)
+    (brl:Rawterm.cases_clauses) avoid : 
     rawconstr build_entry_return = 
   match el with 
     | [] -> assert false (* matched on Nothing !*) 
diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli
index 92df0ec6c3..5dcdb15c5d 100644
--- a/contrib/funind/rawtermops.mli
+++ b/contrib/funind/rawtermops.mli
@@ -22,10 +22,7 @@ val mkRApp  : rawconstr*(rawconstr list) -> rawconstr
 val mkRLambda : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRProd : Names.name*rawconstr*rawconstr -> rawconstr
 val mkRLetIn : Names.name*rawconstr*rawconstr -> rawconstr
-val mkRCases : rawconstr option *
-  (rawconstr * (Names.name * (Util.loc * Names.inductive * Names.name list) option)) list * 
-  (Util.loc * Names.identifier list * cases_pattern list * rawconstr) list -> 
-  rawconstr
+val mkRCases : rawconstr option * tomatch_tuple * cases_clauses -> rawconstr
 val mkRSort : rawsort -> rawconstr 
 val mkRHole : unit -> rawconstr (* we only build Evd.BinderType Anonymous holes *)
 
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index b0de064167..128511c137 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -28,12 +28,8 @@ val rewrite_fixpoint :
   'c
 val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
 val rewrite_cases_aux :
-  Util.loc * Rawterm.rawconstr option *
-  (Rawterm.rawconstr *
-   (Names.name * (Util.loc * Names.inductive * Names.name list) option))
-  list *
-  (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-   Rawterm.rawconstr)
-  list -> Rawterm.rawconstr
+  Util.loc * Rawterm.rawconstr option * 
+  Rawterm.tomatch_tuple * Rawterm.cases_clauses
+  -> Rawterm.rawconstr
 
 val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr