]> matita.cs.unibo.it Git - helm.git/commit
pattern matching over Ast.Case simplified:
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 12 Dec 2008 11:43:39 +0000 (11:43 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 12 Dec 2008 11:43:39 +0000 (11:43 +0000)
commitcf9b09a0c18200c1052648eeace74dc2915706d5
treeb7c3f0b4262cb9d76c3be7922a1151dd7d4734a8
parent99a4ad6d8760a75b7f4464d570cec0e85efe2bb8
pattern matching over Ast.Case simplified:
- it is not possible to match the `in intype` foo part
- it is not possible to match the outtype
eta expansion still done on Ast (hard to do it in Cic. The abstracted variable
does not have a type :-( thus you may have to double your notations. Name for fresh variables changed to \etaX instead of freshX (much shorter in terms of screen pixels)
helm/software/components/acic_content/cicNotationUtil.ml
helm/software/components/acic_content/cicNotationUtil.mli
helm/software/components/content_pres/content2presMatcher.ml