]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 37809db) | patch
Back-porting from new Matita:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Nov 2010 12:49:26 +0000 (12:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Nov 2010 12:49:26 +0000 (12:49 +0000)
commit186638106f23401e88e512a4a6dfd07d73d8be04
tree120a654a638017ddcc2e725d205cce869a856580tree | snapshot
parent37809db7d682ba90ee874b62aee056190d3d5446commit | diff
Back-porting from new Matita:

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.
helm/software/components/ng_tactics/nTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.