]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9e9a16a) | patch
Bug fixed: analysing inductive type that contains implicit used to
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Nov 2010 09:58:42 +0000 (09:58 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 18 Nov 2010 09:58:42 +0000 (09:58 +0000)
commitf5c28fbe41e4754af1c161e7b4176ae053199cc7
treec3ca4ceabf6d6e785cba21df822ec4cc04805302tree | snapshot
parent9e9a16a3568a14f5db43b664d094a66260d5c20acommit | diff
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.
matita/components/ng_tactics/nTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.