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, 2 Jan 2023 19:39:10 +0000 (20:39 +0100)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Mon, 2 Jan 2023 19:39:10 +0000 (20:39 +0100)
commit	8a5c30a914d7ff665218b31853c6fb4bcf58aa08
tree	3aa4fec548011e3d81161e9584876fc230e3cdda	tree \| snapshot
parent	d7aca3eacb4bd8dc56223098f92e5370c82f92ff	commit \| diff

Use of standard OCaml syntax

- do not rely on camlp5o for many files
- comply with the most recent OCaml warnings
- gtkMisc splitted into gtkMisc and gtkMiscCli, the latter
does not depend on Gtk
- matitaclean is no longer a symbolic link to matita
(required to switch to dune)

68 files changed:

matita/components/METAS/meta.helm-grafite_engine.src		diff \| blob \| history
matita/components/METAS/meta.helm-ng_tactics.src		diff \| blob \| history
matita/components/content/notationEnv.ml		diff \| blob \| history
matita/components/content_pres/cicNotationParser.mli		diff \| blob \| history
matita/components/content_pres/cicNotationPres.ml		diff \| blob \| history
matita/components/content_pres/content2presMatcher.ml		diff \| blob \| history
matita/components/content_pres/termContentPres.ml		diff \| blob \| history
matita/components/content_pres/termContentPres.mli		diff \| blob \| history
matita/components/disambiguation/disambiguate.ml		diff \| blob \| history
matita/components/extlib/discrimination_tree.ml		diff \| blob \| history
matita/components/extlib/trie.mli		diff \| blob \| history
matita/components/grafite/grafiteAstPp.ml		diff \| blob \| history
matita/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
matita/components/grafite_engine/nCicCoercDeclaration.ml		diff \| blob \| history
matita/components/grafite_engine/nCicCoercDeclaration.mli		diff \| blob \| history
matita/components/grafite_parser/grafiteParser.mli		diff \| blob \| history
matita/components/library/librarian.ml		diff \| blob \| history
matita/components/ng_cic_content/interpretations.ml		diff \| blob \| history
matita/components/ng_cic_content/interpretations.mli		diff \| blob \| history
matita/components/ng_disambiguation/grafiteDisambiguate.ml		diff \| blob \| history
matita/components/ng_disambiguation/grafiteDisambiguate.mli		diff \| blob \| history
matita/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history
matita/components/ng_extraction/common.mli		diff \| blob \| history
matita/components/ng_extraction/coq.ml		diff \| blob \| history
matita/components/ng_extraction/extraction.mli		diff \| blob \| history
matita/components/ng_extraction/mlutil.mli		diff \| blob \| history
matita/components/ng_extraction/nCicExtraction.ml		diff \| blob \| history
matita/components/ng_extraction/ocaml.mli		diff \| blob \| history
matita/components/ng_extraction/ocamlExtraction.mli		diff \| blob \| history
matita/components/ng_extraction/ocamlExtractionTable.ml		diff \| blob \| history
matita/components/ng_extraction/ocamlExtractionTable.mli		diff \| blob \| history
matita/components/ng_kernel/nCicReduction.ml		diff \| blob \| history
matita/components/ng_library/nCicLibrary.ml		diff \| blob \| history
matita/components/ng_library/nCicLibrary.mli		diff \| blob \| history
matita/components/ng_paramodulation/nCicBlob.mli		diff \| blob \| history
matita/components/ng_paramodulation/nCicParamod.ml		diff \| blob \| history
matita/components/ng_paramodulation/nCicProof.ml		diff \| blob \| history
matita/components/ng_refiner/nCicCoercion.ml		diff \| blob \| history
matita/components/ng_refiner/nCicCoercion.mli		diff \| blob \| history
matita/components/ng_refiner/nCicMetaSubst.ml		diff \| blob \| history
matita/components/ng_refiner/nCicRefiner.ml		diff \| blob \| history
matita/components/ng_refiner/nCicUnifHint.ml		diff \| blob \| history
matita/components/ng_refiner/nCicUnifHint.mli		diff \| blob \| history
matita/components/ng_refiner/nCicUnification.ml		diff \| blob \| history
matita/components/ng_refiner/oMeta2nMeta.ml		diff \| blob \| history
matita/components/ng_tactics/declarative.ml		diff \| blob \| history
matita/components/ng_tactics/nCicElim.ml		diff \| blob \| history
matita/components/ng_tactics/nDestructTac.ml		diff \| blob \| history
matita/components/ng_tactics/nDestructTac.mli		diff \| blob \| history
matita/components/ng_tactics/nTacStatus.ml		diff \| blob \| history
matita/components/ng_tactics/nTacStatus.mli		diff \| blob \| history
matita/components/ng_tactics/nTactics.ml		diff \| blob \| history
matita/components/ng_tactics/nnAuto.ml		diff \| blob \| history
matita/components/syntax_extensions/utf8MacroTable.ml		diff \| blob \| history
matita/components/syntax_extensions/utf8MacroTable.ml.txt		diff \| blob \| history
matita/components/xml/test.ml		diff \| blob \| history
matita/matita/.depend		diff \| blob \| history
matita/matita/.depend.opt		diff \| blob \| history
matita/matita/Makefile		diff \| blob \| history
matita/matita/matitaGtkMisc.ml		diff \| blob \| history
matita/matita/matitaGuiInit.ml		diff \| blob \| history
matita/matita/matitaMisc.ml		diff \| blob \| history
matita/matita/matitaMisc.mli		diff \| blob \| history
matita/matita/matitaMiscCli.ml	[new file with mode: 0644]	blob
matita/matita/matitaMiscCli.mli	[new file with mode: 0644]	blob
matita/matita/matitac.ml		diff \| blob \| history
matita/matita/matitaclean.ml		diff \| blob \| history
matita/matita/matitaclean.mli	[deleted file]	blob \| history

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

RSS Atom