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

1. matitaEngine splitted into disambiguation (now in grafite_parser) and
   in evaluation (now in grafite2)
2. .moo files are now grafite ASTs at the CIC level; they used to be at the
   content (or even presentation?) level
3. coq.ma is no longer a special file; added "-I .." in tests to make them
   include coq.ma

Modified Files in ocaml:
Makefile.in grafite/grafiteAst.ml grafite/grafiteAstPp.ml
grafite/grafiteAstPp.mli grafite/grafiteMarshal.ml
grafite/grafiteMarshal.mli grafite/grafiteParser.ml
grafite/grafiteParser.mli library/libraryClean.ml
Modified Files in matita:
        .depend Makefile.in configure.ac coq.ma dump_moo.ml matita.ml
        matitaEngine.ml matitaEngine.mli matitaExcPp.ml
        matitaGtkMisc.ml matitaGui.ml matitaGuiTypes.mli
        matitaMathView.ml matitaMisc.ml matitaMisc.mli matitaScript.ml
        matitaScript.mli matitaTypes.ml matitaTypes.mli matitacLib.ml
        matitaclean.ml matitadep.ml tests/Makefile
Added Files in ocaml:
METAS/meta.helm-grafite2.src
METAS/meta.helm-grafite_parser.src grafite2/.cvsignore
grafite2/.depend grafite2/Makefile grafite2/disambiguatePp.ml
grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml
grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml
grafite2/grafiteMisc.mli grafite2/grafiteTypes.ml
grafite2/grafiteTypes.mli grafite2/matitaSync.ml
grafite2/matitaSync.mli grafite_parser/.cvsignore
grafite_parser/.depend grafite_parser/Makefile
grafite_parser/grafiteDisambiguate.cmi
grafite_parser/grafiteDisambiguate.cmo
grafite_parser/grafiteDisambiguate.cmx
grafite_parser/grafiteDisambiguate.ml
grafite_parser/grafiteDisambiguate.mli
grafite_parser/grafiteDisambiguate.o
grafite_parser/grafite_parser.a
grafite_parser/grafite_parser.cma
grafite_parser/grafite_parser.cmxa
grafite_parser/matitaDisambiguator.cmi
grafite_parser/matitaDisambiguator.cmo
grafite_parser/matitaDisambiguator.cmx
grafite_parser/matitaDisambiguator.ml
grafite_parser/matitaDisambiguator.mli
grafite_parser/matitaDisambiguator.o
Removed Files in matita:
        disambiguatePp.ml disambiguatePp.mli matitaDisambiguator.ml
        matitaDisambiguator.mli matitaSync.ml matitaSync.mli

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 2 Dec 2005 10:57:02 +0000 (10:57 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 2 Dec 2005 10:57:02 +0000 (10:57 +0000)
commit	a58d25c192ff13ecee2cb92f07ee6f1cbe5219b5
tree	9e73846f756dbfb784218985386e8852a66760a0	tree \| snapshot
parent	1bf23558e2145bcc125102d61f1ca17643d0fd02	commit \| diff

helm/ocaml/METAS/meta.helm-grafite2.src	[new file with mode: 0644]	blob
helm/ocaml/METAS/meta.helm-grafite_parser.src	[new file with mode: 0644]	blob
helm/ocaml/Makefile.in		diff \| blob \| history
helm/ocaml/grafite/grafiteAst.ml		diff \| blob \| history
helm/ocaml/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/ocaml/grafite/grafiteAstPp.mli		diff \| blob \| history
helm/ocaml/grafite/grafiteMarshal.ml		diff \| blob \| history
helm/ocaml/grafite/grafiteMarshal.mli		diff \| blob \| history
helm/ocaml/grafite/grafiteParser.ml		diff \| blob \| history
helm/ocaml/grafite/grafiteParser.mli		diff \| blob \| history
helm/ocaml/grafite2/.cvsignore	[new file with mode: 0644]	blob
helm/ocaml/grafite2/.depend	[new file with mode: 0644]	blob
helm/ocaml/grafite2/Makefile	[new file with mode: 0644]	blob
helm/ocaml/grafite2/disambiguatePp.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite2/disambiguatePp.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteEngine.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteEngine.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteMisc.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteMisc.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteTypes.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite2/grafiteTypes.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite2/matitaSync.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite2/matitaSync.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/.cvsignore	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/.depend	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/Makefile	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.cmi	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.cmo	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.cmx	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafiteDisambiguate.o	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafite_parser.a	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafite_parser.cma	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/grafite_parser.cmxa	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.cmi	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.cmo	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.cmx	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.ml	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.mli	[new file with mode: 0644]	blob
helm/ocaml/grafite_parser/matitaDisambiguator.o	[new file with mode: 0644]	blob
helm/ocaml/library/libraryClean.ml		diff \| blob \| history