]> matita.cs.unibo.it Git - helm.git/commit
BIG FAT COMMIT REGARDING COERCIONS:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 15:51:36 +0000 (15:51 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 4 Sep 2006 15:51:36 +0000 (15:51 +0000)
commitabd2098b6c4a40b36bb4b950c607eb4b4a7852bc
treecce957a84cace0f0eae733eef1bb6f2e184f154a
parent4104453c74bbff05f95003f8d6239f873d1adbf9
BIG FAT COMMIT REGARDING COERCIONS:
- multiple coercions from the same type
- coercions to funclass
- fixed cicPp for letin and pi
- improved coercions ma with a minimal test for funclass
- cheanged XML and Ast to support `Coercion ARITY label
- added syntax:
  coercion URI ARITY
  recordfield :ARITY> type
- added topological sorting module (funcotr) in extlib
- abstracted graphviz to allow non strict and tred graphs
- tentative (not yet properly done) of hiding coercions in content
- fixed a problem in metadata contraints iof there are no constraints
- renamed/moved/commented some functions (eat_prod related) in the refiner
- crossed fingers
47 files changed:
helm/software/components/acic_content/cicNotationPp.ml
helm/software/components/acic_content/cicNotationPt.ml
helm/software/components/acic_content/cicNotationUtil.ml
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/cic/cic.ml
helm/software/components/cic/cicParser.ml
helm/software/components/cic/cicUtil.ml
helm/software/components/cic/cicUtil.mli
helm/software/components/cic_acic/cic2Xml.ml
helm/software/components/cic_acic/cic2acic.ml
helm/software/components/cic_disambiguation/disambiguate.ml
helm/software/components/cic_proof_checking/cicPp.ml
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/cicUnification.ml
helm/software/components/extlib/.depend
helm/software/components/extlib/Makefile
helm/software/components/extlib/graphvizPp.ml
helm/software/components/extlib/graphvizPp.mli
helm/software/components/extlib/hExtlib.ml
helm/software/components/extlib/hExtlib.mli
helm/software/components/extlib/hTopoSort.ml [new file with mode: 0644]
helm/software/components/extlib/hTopoSort.mli [new file with mode: 0644]
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite/grafiteMarshal.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteSync.mli
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/lexicon/lexiconAst.ml
helm/software/components/library/cicCoercion.ml
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/coercGraph.ml
helm/software/components/library/coercGraph.mli
helm/software/components/library/librarySync.ml
helm/software/components/library/librarySync.mli
helm/software/components/metadata/metadataConstraints.ml
helm/software/components/metadata/metadataDeps.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/tactics.mli
helm/software/matita/lablGraphviz.ml
helm/software/matita/lablGraphviz.mli
helm/software/matita/library/legacy/coq.ma
helm/software/matita/library/logic/equality.ma
helm/software/matita/matitaMathView.ml
helm/software/matita/tests/coercions.ma