]> matita.cs.unibo.it Git - helm.git/commit
Patch to add a debugging string to HExtlib.split_nth reverted
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 May 2009 19:37:08 +0000 (19:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 May 2009 19:37:08 +0000 (19:37 +0000)
commit1b70a1f66be53f76e475383e86d63c2b5c1fbcaa
treef45cc5dfb33c065be8a32a141a50dd198a6160e6
parentf49690e1d1b39ccad40f1e874d9d19f6ffc289e0
Patch to add a debugging string to HExtlib.split_nth reverted
(we cannot add a string to every function that raises an exception).

To know where the problem is, it is sufficient to look at the backtrace.
However:
 1) it works for matitac -debug
 2) ocaml is so dumb that it says "compile with -g" when it cannot find
    the executable in the current working directory. Since Matita chdir
    to the directory where the .ma file is, you need to put a copy of
    matitac (or make a symbolic link) where the .ma file is.
19 files changed:
helm/software/components/acic_content/acic2content.ml
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/acic_procedural/procedural2.ml
helm/software/components/acic_procedural/proceduralOptimizer.ml
helm/software/components/cic_proof_checking/cicDischarge.ml
helm/software/components/cic_proof_checking/cicTypeChecker.ml
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/content_pres/content2pres.ml
helm/software/components/extlib/hExtlib.ml
helm/software/components/extlib/hExtlib.mli
helm/software/components/metadata/metadataDeps.ml
helm/software/components/ng_kernel/nCicReduction.ml
helm/software/components/ng_kernel/nCicTypeChecker.ml
helm/software/components/ng_kernel/oCic2NCic.ml
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicUnification.ml
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/tactics/closeCoercionGraph.ml
helm/software/components/tactics/destructTactic.ml