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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Mon, 20 Apr 2009 07:58:14 +0000 (07:58 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Mon, 20 Apr 2009 07:58:14 +0000 (07:58 +0000)
commit	7cb22a7f8107a6cde0b77b7879e04f586a347102
tree	09321e6534edfbf142ec55c6742541db8bf78a5e	tree \| snapshot
parent	cb25e0f32f7581e1a49d1d1c109108763dfb882c	commit \| diff

- init_cache_and_tables rewritten using the automation_cache
- new moo command Select to index an equality
- new command pump to perform some given clause steps on the automation
  cache tables
- no more imperative maxmeta in paramodulation:
  - paramodulation/* forlds a bag containing it
  - auto.ml folds tables, containing a bag

29 files changed:

helm/software/components/binaries/transcript/.depend		diff \| blob \| history
helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite/grafiteMarshal.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteSync.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/tactics/.depend		diff \| blob \| history
helm/software/components/tactics/.depend.opt		diff \| blob \| history
helm/software/components/tactics/auto.ml		diff \| blob \| history
helm/software/components/tactics/automationCache.ml		diff \| blob \| history
helm/software/components/tactics/automationCache.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/equality.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/indexing.mli		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.ml		diff \| blob \| history
helm/software/components/tactics/paramodulation/saturation.mli		diff \| blob \| history
helm/software/components/tactics/universe.ml		diff \| blob \| history
helm/software/components/tactics/universe.mli		diff \| blob \| history
helm/software/matita/library/demo/power_derivative.ma		diff \| blob \| history
helm/software/matita/library/demo/propositional_sequent_calculus.ma		diff \| blob \| history
helm/software/matita/library/didactic/exercises/duality.ma		diff \| blob \| history
helm/software/matita/library/didactic/exercises/shannon.ma		diff \| blob \| history
helm/software/matita/library/didactic/exercises/substitution.ma		diff \| blob \| history
helm/software/matita/library/nat/gcd.ma		diff \| blob \| history
helm/software/matita/library/nat/ord.ma		diff \| blob \| history
helm/software/matita/library/nat/times.ma		diff \| blob \| history

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

RSS Atom