]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b4b4e4a) | patch
Debugging code to understand cases where the output notation is not
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 30 May 2011 11:02:26 +0000 (11:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 30 May 2011 11:02:26 +0000 (11:02 +0000)
commit10c62d5b6703eddbc83b011b73f9540e47a2001f
treef07cb5431c48f93cfd443036dfca0ef67625c7d7tree | snapshot
parentb4b4e4ae04986f2e344e403191e957c1f4b185aacommit | diff
Debugging code to understand cases where the output notation is not
applied, is applied badly or it raises an assert failure.

Usually the problem is given by optional parts of the term. For instance,
in output all typing information is present and it _must_ be matched.
matita/components/content_pres/content2presMatcher.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.