matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Mon, 20 May 2002 08:39:06 +0000 (08:39 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Mon, 20 May 2002 08:39:06 +0000 (08:39 +0000)
commit	37f08b2aba9f17d9d609ca0f57d607f437a3d3fc
tree	9c25bbf5768aea0963a1ab29230c0eab76853cfd	tree \| snapshot
parent	a61f397a3ea3acaf95a04a2aafbf1d3f223a2755	commit \| diff

New experimental commit: metavariables representation is changed again,
together with the DTD (still uncommitted). The new representation implements
explicit substitutions, allowing the correct reduction behaviour.
The most part of the modules have been changed to reflect the new
representation. Unification has been rewritten.

23 files changed:

helm/ocaml/cic/cic.ml		diff \| blob \| history
helm/ocaml/cic/cicParser.ml		diff \| blob \| history
helm/ocaml/cic/cicParser2.ml		diff \| blob \| history
helm/ocaml/cic/cicParser3.ml		diff \| blob \| history
helm/ocaml/cic/deannotate.ml		diff \| blob \| history
helm/ocaml/cic_annotations/cicAnnotation2Xml.ml		diff \| blob \| history
helm/ocaml/cic_annotations/cicXPath.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/.cvsignore		diff \| blob \| history
helm/ocaml/cic_proof_checking/.depend		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicPp.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicPp.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionMachine.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicReductionNaif.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicSubstitution.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicSubstitution.mli		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.ml		diff \| blob \| history
helm/ocaml/cic_proof_checking/cicTypeChecker.mli		diff \| blob \| history
helm/ocaml/cic_textual_parser/cicTextualLexer.mll		diff \| blob \| history
helm/ocaml/cic_textual_parser/cicTextualParser.mly		diff \| blob \| history
helm/ocaml/cic_textual_parser/cicTextualParser0.ml		diff \| blob \| history
helm/ocaml/cic_textual_parser/cicTextualParserContext.mli		diff \| blob \| history
helm/ocaml/cic_unification/cicUnification.ml		diff \| blob \| history
helm/ocaml/cic_unification/cicUnification.mli		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom