]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 38633ee) | patch
bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 29 Nov 2004 12:22:23 +0000 (12:22 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 29 Nov 2004 12:22:23 +0000 (12:22 +0000)
commita785a3526d4dcbb6c5810ed4fb943132c9ff2d45
tree33b56ac1d914362b378e843d99290e54dd940ef0tree | snapshot
parent38633ee024797543bba347addb8f287fd3e5331fcommit | diff
bugfix: FreshNameGenerator uses the type checker on mk_fresh_name
invocation, thus it should receive in input a subst to be passed to the
type checker in order to avoid "unknown" Metas in the term to be type
checked
helm/ocaml/cic_unification/freshNamesGenerator.ml diff | blob | history
helm/ocaml/cic_unification/freshNamesGenerator.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.