]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5dbc68) | patch
When we unify a Prod against a term t2 which is not a Prod we
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2005 15:26:55 +0000 (15:26 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 20 May 2005 15:26:55 +0000 (15:26 +0000)
commitd1d5e134c680aaa1cab15a35b944ca0a3a39c704
tree1f5f518cbd39e2a62d1537585862c9d249294641tree | snapshot
parentc5dbc685d2ef5c3b929efefda75478c59eac6fefcommit | diff
When we unify a Prod against a term t2 which is not a Prod we
now try a whd of t2.
helm/ocaml/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.