]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c9a4185) | patch
- fixed hint generation, more hints are generated
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Mar 2009 20:16:35 +0000 (20:16 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 3 Mar 2009 20:16:35 +0000 (20:16 +0000)
commit7bc72d8afaebb1d2070a26b07f9bf4242b648e2c
treec9c31f209ff6fe1f2590724cda3e962bc769be5atree | snapshot
parentc9a4185ac1fef28e5741b8671abf02e33d04ac0dcommit | diff
- fixed hint generation, more hints are generated
- fixpoint refinement added
- Appl [Meta _; ... ] handled correctly, no double Appl or Beta redex is
  generated (both in regular code and interators)
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/ng_disambiguation/nCicDisambiguate.ml diff | blob | history
helm/software/components/ng_disambiguation/nCicDisambiguate.mli diff | blob | history
helm/software/components/ng_kernel/nCicReduction.ml diff | blob | history
helm/software/components/ng_kernel/nCicReduction.mli diff | blob | history
helm/software/components/ng_kernel/nCicUntrusted.ml diff | blob | history
helm/software/components/ng_kernel/nCicUtils.ml diff | blob | history
helm/software/components/ng_kernel/nCicUtils.mli diff | blob | history
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnifHint.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.