]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 05e6e47) | patch
- too strict check on left parameters of constructors in guarded by constructors...
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 25 Jul 2008 17:01:49 +0000 (17:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 25 Jul 2008 17:01:49 +0000 (17:01 +0000)
commitf1ce4df54ccdeba41d69a6366b4ad2b970a02773
treef96f780421ffdf57d2489fee5389470aaa496b29tree | snapshot
parent05e6e4771934d95be8b4cffcc87eeb7b27250536commit | diff
- too strict check on left parameters of constructors in guarded by constructors removed
- the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the
  new kernel since:
    o  recursive/corecursive objects are now closed terms
    o  we do not allow (yet?) to pass co-recursive functions around
    o  we do check that the arguments of the application of a fix/cofix do not
       contain the function we are checking for GBC
helm/software/components/ng_kernel/nCicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.