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

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

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Fri, 30 Dec 2022 01:19:16 +0000 (02:19 +0100)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Tue, 14 Feb 2023 14:22:45 +0000 (15:22 +0100)
commit	6b76c5b3b82753966cabffd8536d8dd9f8cada20
tree	0ff960be5a1510066841188c0b12b2118e022bc9	tree \| snapshot
parent	aa5c8c99c9f7ae285883cff133fc02b3d064888c	commit \| diff

Porting to ocaml 5

- old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation
- as a consequence, bytecode is now compile in -custom mode
- requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5
(all currently not accepted upstream yet)
- plenty of new warnings either turned off or applied to code
- ported to most recent version of camlp5

74 files changed:

matita/components/METAS/meta.helm-ng_paramodulation.src		diff \| blob \| history
matita/components/METAS/meta.helm-thread.src		diff \| blob \| history
matita/components/METAS/meta.helm-xml.src		diff \| blob \| history
matita/components/Makefile.common		diff \| blob \| history
matita/components/binaries/matitaprover/matitaprover.ml		diff \| blob \| history
matita/components/content/.depend.opt		diff \| blob \| history
matita/components/content_pres/.depend.opt		diff \| blob \| history
matita/components/content_pres/cicNotationParser.ml		diff \| blob \| history
matita/components/disambiguation/.depend.opt		diff \| blob \| history
matita/components/disambiguation/disambiguateTypes.ml		diff \| blob \| history
matita/components/extlib/.depend.opt		diff \| blob \| history
matita/components/extlib/patternMatcher.ml		diff \| blob \| history
matita/components/getter/.depend.opt		diff \| blob \| history
matita/components/getter/http_getter_misc.ml		diff \| blob \| history
matita/components/getter/http_getter_storage.ml		diff \| blob \| history
matita/components/grafite/.depend.opt		diff \| blob \| history
matita/components/grafite_engine/.depend.opt		diff \| blob \| history
matita/components/grafite_parser/.depend.opt		diff \| blob \| history
matita/components/grafite_parser/print_grammar.ml		diff \| blob \| history
matita/components/library/.depend.opt		diff \| blob \| history
matita/components/library/libraryClean.ml		diff \| blob \| history
matita/components/logger/.depend.opt		diff \| blob \| history
matita/components/ng_cic_content/.depend.opt		diff \| blob \| history
matita/components/ng_cic_content/interpretations.ml		diff \| blob \| history
matita/components/ng_disambiguation/.depend.opt		diff \| blob \| history
matita/components/ng_disambiguation/nCicDisambiguate.ml		diff \| blob \| history
matita/components/ng_extraction/.depend.opt		diff \| blob \| history
matita/components/ng_kernel/.depend.opt		diff \| blob \| history
matita/components/ng_kernel/nCicReduction.ml		diff \| blob \| history
matita/components/ng_kernel/nCicUntrusted.ml		diff \| blob \| history
matita/components/ng_kernel/nReference.ml		diff \| blob \| history
matita/components/ng_library/.depend.opt		diff \| blob \| history
matita/components/ng_paramodulation/.depend.opt		diff \| blob \| history
matita/components/ng_paramodulation/Makefile		diff \| blob \| history
matita/components/ng_paramodulation/foUtils.ml		diff \| blob \| history
matita/components/ng_paramodulation/hash.c	[new file with mode: 0644]	blob
matita/components/ng_paramodulation/index.ml		diff \| blob \| history
matita/components/ng_paramodulation/nCicBlob.ml		diff \| blob \| history
matita/components/ng_paramodulation/orderings.ml		diff \| blob \| history
matita/components/ng_paramodulation/stats.ml		diff \| blob \| history
matita/components/ng_paramodulation/terms.ml		diff \| blob \| history
matita/components/ng_refiner/.depend.opt		diff \| blob \| history
matita/components/ng_refiner/nCicCoercion.ml		diff \| blob \| history
matita/components/ng_refiner/nCicUnifHint.ml		diff \| blob \| history
matita/components/ng_refiner/nCicUnification.ml		diff \| blob \| history
matita/components/ng_refiner/nDiscriminationTree.ml		diff \| blob \| history
matita/components/ng_tactics/.depend.opt		diff \| blob \| history
matita/components/ng_tactics/nTacStatus.ml		diff \| blob \| history
matita/components/ng_tactics/nnAuto.ml		diff \| blob \| history
matita/components/registry/.depend.opt		diff \| blob \| history
matita/components/registry/helm_registry.ml		diff \| blob \| history
matita/components/syntax_extensions/.depend		diff \| blob \| history
matita/components/syntax_extensions/.depend.opt		diff \| blob \| history
matita/components/syntax_extensions/Makefile		diff \| blob \| history
matita/components/syntax_extensions/utf8Macro.ml		diff \| blob \| history
matita/components/syntax_extensions/utf8MacroTable.mli	[new file with mode: 0644]	blob
matita/components/thread/.depend.opt		diff \| blob \| history
matita/components/thread/extThread.ml		diff \| blob \| history
matita/components/xml/.depend.opt		diff \| blob \| history
matita/configure.ac		diff \| blob \| history
matita/matita/.depend.opt		diff \| blob \| history
matita/matita/Makefile		diff \| blob \| history
matita/matita/cicMathView.ml		diff \| blob \| history
matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml		diff \| blob \| history
matita/matita/matitaExcPp.ml		diff \| blob \| history
matita/matita/matitaGtkMisc.mli		diff \| blob \| history
matita/matita/matitaGui.ml		diff \| blob \| history
matita/matita/matitaInit.ml		diff \| blob \| history
matita/matita/matitaMathView.ml		diff \| blob \| history
matita/matita/matitaMathView.mli		diff \| blob \| history
matita/matita/matitaMisc.ml		diff \| blob \| history
matita/matita/matitaMisc.mli		diff \| blob \| history
matita/matita/matitaScript.ml		diff \| blob \| history
matita/matita/predefined_virtuals.ml		diff \| blob \| history

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

RSS Atom