]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7cdfae2) | patch
- pretty printer made robust in face of list_nth
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 5 May 2009 16:56:33 +0000 (16:56 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 5 May 2009 16:56:33 +0000 (16:56 +0000)
commit1bd6b7d2637d765f11ddbd1218d63474e9d0c63b
tree4efd2e4c3facb8e01b8c81bc7697f6a835e4a685tree | snapshot
parent7cdfae2ec209750303818f2e39f31e4739286858commit | diff
- pretty printer made robust in face of list_nth
- bugfixed in generation of aliases in nCicLibrary:
  contructor index are 1-based
- refinement of indtypes fixed:
  - missing undebujinate added
  - index for current indty was in the wrong order
- apply_subst moved to nCicUntrusted
- new iterator for obj_kind
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.ml diff | blob | history
helm/software/components/ng_kernel/nCicPp.ml diff | blob | history
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
helm/software/components/ng_kernel/nCicUntrusted.ml diff | blob | history
helm/software/components/ng_kernel/nCicUntrusted.mli diff | blob | history
helm/software/components/ng_refiner/nCicRefiner.ml diff | blob | history
helm/software/components/ng_tactics/nTacStatus.ml diff | blob | history
helm/software/components/ng_tactics/nTacStatus.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.