]> matita.cs.unibo.it Git - helm.git/commitdiff
* env renamed to context everywhere in cicTypeChecker.ml
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Apr 2002 16:53:48 +0000 (16:53 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 19 Apr 2002 16:53:48 +0000 (16:53 +0000)
* Definitions should be allowed in the contexts as well as Declarations.
  This is the very first step: the notion of context is introduced in cic.ml
  and the interface of cicTypeChecker.mli reflects that. (Of course, also the
  interface of cicReduction should do the same!)
  The new implementation just raises an exception when a definition is found
  in the context.


No differences found