]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 977faf4) | patch
- static disambiguation of Automath unified binders
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 24 Nov 2014 23:07:39 +0000 (23:07 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 24 Nov 2014 23:07:39 +0000 (23:07 +0000)
commit39cf453a20e35416d0fd932cc5bf14733e918587
tree20b3d835ba61bf7b9778ecb947b7e341078695a2tree | snapshot
parent977faf4820cd8ff5e2f0a5249161bbb92ae4b097commit | diff
- static disambiguation of Automath unified binders
  by position heuristics + degree heuristics fixed
  [ grundlagen_2: now 1217 binders out of 47115 remain ambiguous ]
- brgReduction: we did not check the sort-inclusion flag
- new constraints system continues ...
helm/software/helena/.depend.opt diff | blob | history
helm/software/helena/Makefile diff | blob | history
helm/software/helena/src/automath/autCrg.ml diff | blob | history
helm/software/helena/src/automath/autCrg.mli diff | blob | history
helm/software/helena/src/basic_rg/brgReduction.ml diff | blob | history
helm/software/helena/src/common/level.ml diff | blob | history
helm/software/helena/src/common/marks.ml diff | blob | history
helm/software/helena/src/common/status.ml diff | blob | history
helm/software/helena/src/toplevel/top.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.