]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6b3698) | patch
sort_of_prod now thinks that a "sort metavariable" is a metavariable where
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Feb 2004 16:40:29 +0000 (16:40 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 9 Feb 2004 16:40:29 +0000 (16:40 +0000)
commitfb153b0a3853478410bfbcad98065f1b1610d17d
treecbc9edbefedd07cdb2ffcbbf7e8bc0234d3678a4tree | snapshot
parenta6b369829925668130b977a0abd737bf34ae74bacommit | diff
sort_of_prod now thinks that a "sort metavariable" is a metavariable where
no free variable occurs in the local context. Reason: there used to be a bug
induced by the fact that a metavariable ?1 with an empty canonical context
could be istantiated with a metavariable ?2[l] where l has no free variables
but still it is not of length 0.
helm/ocaml/cic_proof_checking/cicTypeChecker.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.