diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 22:22:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 22:22:15 +0000 |
| commit | 1919b8adc78291b534a611f7bac2874207cb21cb (patch) | |
| tree | c512a78ceda5301f760a8f1fabbeaf3fe82296d2 /contrib/funind | |
| parent | 7b4b2dc4c80a6172692c321468edf46564ae40fb (diff) | |
- 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
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 6 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.mli | 5 |
2 files changed, 3 insertions, 8 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 !*) diff --git a/contrib/funind/rawtermops.mli b/contrib/funind/rawtermops.mli index 92df0ec6c..5dcdb15c5 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 *) |