]> matita.cs.unibo.it Git - helm.git/commit
Merge of the V7_3_new_exportation branch.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jun 2003 15:31:51 +0000 (15:31 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 19 Jun 2003 15:31:51 +0000 (15:31 +0000)
commitbac72fcaa876137ab7a5630e0c1badc2a627dce8
tree381e82c988c4c3bdc86530313479ad635362f94a
parent2dc0733271cd251aaa3edaece8a883fe691775ab
Merge of the V7_3_new_exportation branch.
168 files changed:
helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/applyStylesheets.ml [new file with mode: 0644]
helm/gTopLevel/applyStylesheets.mli [new file with mode: 0644]
helm/gTopLevel/cic2Xml.ml
helm/gTopLevel/cic2Xml.mli
helm/gTopLevel/cic2acic.ml
helm/gTopLevel/cic2acic.mli
helm/gTopLevel/dictionary-cic.xml [new file with mode: 0644]
helm/gTopLevel/disambiguate.ml [new file with mode: 0644]
helm/gTopLevel/disambiguate.mli [new file with mode: 0644]
helm/gTopLevel/doubleTypeInference.ml
helm/gTopLevel/esempi/and_implies_or2.cic
helm/gTopLevel/esempi/apply.cic
helm/gTopLevel/esempi/bug.cic
helm/gTopLevel/esempi/calcolo_proposizioni.cic
helm/gTopLevel/esempi/conversion.cic
helm/gTopLevel/esempi/decompose.cic [new file with mode: 0644]
helm/gTopLevel/esempi/elim.cic
helm/gTopLevel/esempi/elim2.cic
helm/gTopLevel/esempi/evars.cic
helm/gTopLevel/esempi/fourier/fourier.cic [new file with mode: 0644]
helm/gTopLevel/esempi/fourier/fourier_benchmarks.cic [new file with mode: 0644]
helm/gTopLevel/esempi/fourier/fourier_make_benchmarks.ml [new file with mode: 0644]
helm/gTopLevel/esempi/prova.cic
helm/gTopLevel/esempi/sets.cic
helm/gTopLevel/esempi/various.cic [new file with mode: 0644]
helm/gTopLevel/fourier.ml [deleted file]
helm/gTopLevel/fourierR.mli [deleted file]
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/hbugs.ml [new file with mode: 0644]
helm/gTopLevel/hbugs.mli [new file with mode: 0644]
helm/gTopLevel/invokeTactics.ml [new file with mode: 0644]
helm/gTopLevel/invokeTactics.mli [new file with mode: 0644]
helm/gTopLevel/mQueryGenerator.mli [deleted file]
helm/gTopLevel/misc.ml [new file with mode: 0644]
helm/gTopLevel/misc.mli [new file with mode: 0644]
helm/gTopLevel/primitiveTactics.ml [deleted file]
helm/gTopLevel/primitiveTactics.mli [deleted file]
helm/gTopLevel/proofEngine.ml
helm/gTopLevel/proofEngine.mli
helm/gTopLevel/proofEngineHelpers.ml [deleted file]
helm/gTopLevel/proofEngineHelpers.mli [deleted file]
helm/gTopLevel/proofEngineReduction.ml [deleted file]
helm/gTopLevel/proofEngineReduction.mli [deleted file]
helm/gTopLevel/proofEngineStructuralRules.ml [deleted file]
helm/gTopLevel/proofEngineStructuralRules.mli [deleted file]
helm/gTopLevel/proofEngineTypes.ml [deleted file]
helm/gTopLevel/ring.ml [deleted file]
helm/gTopLevel/ring.mli [deleted file]
helm/gTopLevel/sequentPp.ml
helm/gTopLevel/tacticals.ml [deleted file]
helm/gTopLevel/tacticals.mli [deleted file]
helm/gTopLevel/termEditor.ml [new file with mode: 0644]
helm/gTopLevel/termEditor.mli [new file with mode: 0644]
helm/gTopLevel/termViewer.ml [new file with mode: 0644]
helm/gTopLevel/termViewer.mli [new file with mode: 0644]
helm/gTopLevel/texTermEditor.ml [new file with mode: 0644]
helm/gTopLevel/texTermEditor.mli [new file with mode: 0644]
helm/gTopLevel/topLevel/.depend [deleted file]
helm/gTopLevel/topLevel/Makefile [deleted file]
helm/gTopLevel/topLevel/esempi.cic [deleted file]
helm/gTopLevel/xml2Gdome.ml
helm/ocaml/.cvsignore
helm/ocaml/META.helm-tactics.src [new file with mode: 0644]
helm/ocaml/META.helm-tex_cic_textual_parser.src [new file with mode: 0644]
helm/ocaml/Makefile.common.in
helm/ocaml/Makefile.in
helm/ocaml/cic/cic.ml
helm/ocaml/cic/cicParser.ml
helm/ocaml/cic/cicParser.mli
helm/ocaml/cic/cicParser2.ml
helm/ocaml/cic/cicParser2.mli
helm/ocaml/cic/cicParser3.ml
helm/ocaml/cic/cicParser3.mli
helm/ocaml/cic/deannotate.ml
helm/ocaml/cic/deannotate.mli
helm/ocaml/cic_annotations/cicAnnotation2Xml.ml
helm/ocaml/cic_annotations/cicAnnotationParser.ml
helm/ocaml/cic_annotations/cicXPath.ml
helm/ocaml/cic_annotations_cache/cicCache.ml
helm/ocaml/cic_cache/cicCache.ml
helm/ocaml/cic_proof_checking/.cvsignore
helm/ocaml/cic_proof_checking/.depend
helm/ocaml/cic_proof_checking/Makefile
helm/ocaml/cic_proof_checking/cicCooking.ml [deleted file]
helm/ocaml/cic_proof_checking/cicCooking.mli [deleted file]
helm/ocaml/cic_proof_checking/cicEnvironment.ml
helm/ocaml/cic_proof_checking/cicEnvironment.mli
helm/ocaml/cic_proof_checking/cicMiniReduction.ml
helm/ocaml/cic_proof_checking/cicPp.ml
helm/ocaml/cic_proof_checking/cicReduction.mli
helm/ocaml/cic_proof_checking/cicReductionMachine.ml
helm/ocaml/cic_proof_checking/cicReductionMachine.mli
helm/ocaml/cic_proof_checking/cicReductionNaif.ml
helm/ocaml/cic_proof_checking/cicReductionNaif.mli
helm/ocaml/cic_proof_checking/cicSubstitution.ml
helm/ocaml/cic_proof_checking/cicSubstitution.mli
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.mli
helm/ocaml/cic_proof_checking/logger.ml
helm/ocaml/cic_proof_checking/logger.mli
helm/ocaml/cic_textual_parser/.depend
helm/ocaml/cic_textual_parser/cicTextualLexer.mll
helm/ocaml/cic_textual_parser/cicTextualParser.mly
helm/ocaml/cic_textual_parser/cicTextualParser0.ml
helm/ocaml/cic_textual_parser/cicTextualParserContext.ml
helm/ocaml/cic_textual_parser/cicTextualParserContext.mli
helm/ocaml/cic_unification/.depend
helm/ocaml/cic_unification/Makefile
helm/ocaml/cic_unification/cicRefine.ml [new file with mode: 0644]
helm/ocaml/cic_unification/cicRefine.mli [new file with mode: 0644]
helm/ocaml/cic_unification/cicUnification.ml
helm/ocaml/cic_unification/cicUnification.mli
helm/ocaml/getter/.depend
helm/ocaml/getter/clientHTTP.ml
helm/ocaml/getter/configuration.ml
helm/ocaml/getter/configuration.mli
helm/ocaml/getter/getter.ml
helm/ocaml/getter/getter.mli
helm/ocaml/tactics/.cvsignore [new file with mode: 0644]
helm/ocaml/tactics/.depend [new file with mode: 0644]
helm/ocaml/tactics/Makefile [new file with mode: 0644]
helm/ocaml/tactics/discriminationTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/discriminationTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/eliminationTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/eliminationTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/equalityTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/equalityTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/fourier.ml [new file with mode: 0644]
helm/ocaml/tactics/fourier.mli [new file with mode: 0644]
helm/ocaml/tactics/fourierR.ml [new file with mode: 0644]
helm/ocaml/tactics/fourierR.mli [new file with mode: 0644]
helm/ocaml/tactics/introductionTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/introductionTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/negationTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/negationTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/primitiveTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/primitiveTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/proofEngineHelpers.ml [new file with mode: 0644]
helm/ocaml/tactics/proofEngineHelpers.mli [new file with mode: 0644]
helm/ocaml/tactics/proofEngineReduction.ml [new file with mode: 0644]
helm/ocaml/tactics/proofEngineReduction.mli [new file with mode: 0644]
helm/ocaml/tactics/proofEngineStructuralRules.ml [new file with mode: 0644]
helm/ocaml/tactics/proofEngineStructuralRules.mli [new file with mode: 0644]
helm/ocaml/tactics/proofEngineTypes.ml [new file with mode: 0644]
helm/ocaml/tactics/reductionTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/reductionTactics.mli [new file with mode: 0644]
helm/ocaml/tactics/ring.ml [new file with mode: 0644]
helm/ocaml/tactics/ring.mli [new file with mode: 0644]
helm/ocaml/tactics/tacticChaser.ml [new file with mode: 0644]
helm/ocaml/tactics/tacticChaser.mli [new file with mode: 0644]
helm/ocaml/tactics/tacticals.ml [new file with mode: 0644]
helm/ocaml/tactics/tacticals.mli [new file with mode: 0644]
helm/ocaml/tactics/variousTactics.ml [new file with mode: 0644]
helm/ocaml/tactics/variousTactics.mli [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/.cvsignore [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/.depend [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/Makefile [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/texCicTextualParser0.ml [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.ml [new file with mode: 0644]
helm/ocaml/tex_cic_textual_parser/texCicTextualParserContext.mli [new file with mode: 0644]
helm/ocaml/urimanager/uriManager.ml
helm/ocaml/urimanager/uriManager.mli
helm/ocaml/xml/xml.ml
helm/ocaml/xml/xml.mli