- 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

1 files changed, 2 insertions, 4 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 1234c7faa..681e43af0 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 !*)