]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be4ee40) | patch
Restrict reimplemented to avoid generating lists of indexes to be restricted
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 10:59:11 +0000 (10:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Feb 2004 10:59:11 +0000 (10:59 +0000)
commitbe29c5ff666db0960737c0ba2d28a4aa4b2ac246
treec733f3c5e715be853b7958cc615ee292393dfe87tree | snapshot
parentbe4ee4049f0da7dd4131c3f2c56c7d1f46c87ba7commit | diff
Restrict reimplemented to avoid generating lists of indexes to be restricted
that fall outside the context. It doesn't change much, really.
helm/ocaml/cic_unification/cicMetaSubst.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.