]> matita.cs.unibo.it Git - helm.git/commit
* 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)
commit7db7305941a97d43480cf58c08a154ed79f300cb
tree2e5ef800ba1125abbab84b05f23c39a78077a2af
parent797425e905a9d26bb21f18d234a34ed211bcf92c
* env renamed to context everywhere in cicTypeChecker.ml
* 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.
helm/ocaml/cic/cic.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.mli