]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 10634c4) | patch
raise uncertain when a sort is not a sort but may be, use max for mixing universes...
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 9 Dec 2008 18:29:37 +0000 (18:29 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 9 Dec 2008 18:29:37 +0000 (18:29 +0000)
commit63e7ef727ce32552106c4d8f3030fd264532fffe
treeca545569db14abc6d749cad5e1344a902fb7f1a7tree | snapshot
parent10634c47be2ece4c088a1a1c1be5163952bf1c42commit | diff
raise uncertain when a sort is not a sort but may be, use max for mixing universes, coercions to sort in the prod case are triggered before putting the source type in the context
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.