]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 172588c) | patch
- tactics:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)
commit3f586b01da59fe16b3d7f37da28bdd71f2225131
treea379f8b22eaf9e74f323f0c12873beefab712729tree | snapshot
parent172588c02ff4d9ed5cc03265c2bd6a36f8a0f5dacommit | diff
- tactics:
  rename tactic enabled,
  rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
  now starts directly from acic bypassing the content level,
  the script for the use case proof in matita/contribs/prova.ma is reconstructed  completely now and is correctly parsed and typechecked
27 files changed:
components/content_pres/.depend diff | blob | history
components/content_pres/Makefile diff | blob | history
components/content_pres/acic2Procedural.ml [new file with mode: 0644] blob
components/content_pres/acic2Procedural.mli [new file with mode: 0644] blob
components/content_pres/cicClassify.ml [new file with mode: 0644] blob
components/content_pres/cicClassify.mli [new file with mode: 0644] blob
components/content_pres/content2Procedural.ml [deleted file] blob | history
components/content_pres/content2Procedural.mli [deleted file] blob | history
components/content_pres/objPp.ml diff | blob | history
components/content_pres/proceduralTypes.ml [new file with mode: 0644] blob
components/content_pres/proceduralTypes.mli [new file with mode: 0644] blob
components/grafite/grafiteAst.ml diff | blob | history
components/grafite/grafiteAstPp.ml diff | blob | history
components/grafite_engine/grafiteEngine.ml diff | blob | history
components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
components/grafite_parser/grafiteParser.ml diff | blob | history
components/tactics/auto.ml diff | blob | history
components/tactics/discriminationTactics.ml diff | blob | history
components/tactics/equalityTactics.ml diff | blob | history
components/tactics/equalityTactics.mli diff | blob | history
components/tactics/fourierR.ml diff | blob | history
components/tactics/proofEngineStructuralRules.ml diff | blob | history
components/tactics/proofEngineStructuralRules.mli diff | blob | history
components/tactics/tactics.ml diff | blob | history
components/tactics/tactics.mli diff | blob | history
matita/contribs/prova.ma diff | blob | history
matita/matita.lang diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.