]> matita.cs.unibo.it Git - helm.git/commit
disambiguation now returns and takes in input the substitution
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 21 Nov 2008 15:15:43 +0000 (15:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 21 Nov 2008 15:15:43 +0000 (15:15 +0000)
commit424982ded255df68245241f56064202844ed1194
treec3c1f9d3a509e40fae8c274d32108a901bc035a9
parentc17c73bcba0d18bb3f6ccf9fb3fad8c363652541
disambiguation now returns and takes in input the substitution
helm/software/components/cic_disambiguation/disambiguate.ml
helm/software/components/cic_disambiguation/disambiguate.mli
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteDisambiguator.ml
helm/software/components/ng_disambiguation/nDisambiguate.ml
helm/software/components/ng_refiner/nCicRefiner.mli