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>
	Fri, 30 Dec 2022 01:50:59 +0000 (02:50 +0100)
commit	e082eec771e24842f29a01fa258f7c80bc2db599
tree	c2d83c4aba00a3c58e99d4dc733f988cb7ae3ad4	tree \| snapshot
parent	2815c74c03f38089d0e27aba00e2280223b0f76f	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