]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7090733) | patch
- removed metasenv argument from kernel proxies invocations
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 2 Feb 2004 16:37:10 +0000 (16:37 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 2 Feb 2004 16:37:10 +0000 (16:37 +0000)
commit335186953e826833ed43b33cac98884d3f99a228
tree4d0322bba1dcbae0e60c4c6a193d7c819e86426btree | snapshot
parent7090733367302ff4f9c53e8b3a1b82109a086fbfcommit | diff
- removed metasenv argument from kernel proxies invocations
- lift_meta over defs with an explicit type implemented
- reimplemented eat_prods (open bug: when an application has more than
  one argument and its type is a meta then the outtype is a Meta whose
  context is not general enough. To be implemented)
helm/ocaml/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.