]> matita.cs.unibo.it Git - helm.git/commit
disambiguation can use a goal as hint for the expected type
authorEnrico Tassi <enrico.tassi@inria.fr>
Sat, 15 Nov 2008 12:53:35 +0000 (12:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Sat, 15 Nov 2008 12:53:35 +0000 (12:53 +0000)
commit154cbc049da8d8c3dd090a919a40c90eb23cc24e
tree2a0a81a38720deb7ce2a45f85fb4836d939026d0
parent88f24d23df67d88bf98c2ca32ac0d9854f3d9b00
disambiguation can use a goal as hint for the expected type
helm/software/components/cic_disambiguation/disambiguate.ml
helm/software/components/cic_disambiguation/disambiguate.mli
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteDisambiguate.mli
helm/software/components/grafite_parser/grafiteDisambiguator.ml
helm/software/components/grafite_parser/grafiteParser.ml