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

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

author	Stefano Zacchiroli <zack@upsilon.cc>
	Thu, 8 Sep 2005 10:42:03 +0000 (10:42 +0000)
committer	Stefano Zacchiroli <zack@upsilon.cc>
	Thu, 8 Sep 2005 10:42:03 +0000 (10:42 +0000)
commit	d1126c6b78a3333bbf415daf027004496b77c2f4
tree	4998aa6bbda2053f261cc4f0f4d0a095f59d647e	tree \| snapshot
parent	0b082b38f60079c8d457790c3ee18c2a9ab415eb	commit \| diff

implemented lazy disambiguation of tactics arguments, when those
arguments have to be parsed in contexts extracted by a pattern

20 files changed:

helm/matita/matitaEngine.ml		diff \| blob \| history
helm/matita/matitaEngine.mli		diff \| blob \| history
helm/matita/matitaMisc.mli		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.ml		diff \| blob \| history
helm/ocaml/cic_disambiguation/disambiguateTypes.mli		diff \| blob \| history
helm/ocaml/cic_notation/grafiteAst.ml		diff \| blob \| history
helm/ocaml/cic_notation/grafiteAstPp.mli		diff \| blob \| history
helm/ocaml/cic_notation/grafiteParser.mli		diff \| blob \| history
helm/ocaml/tactics/discriminationTactics.ml		diff \| blob \| history
helm/ocaml/tactics/equalityTactics.ml		diff \| blob \| history
helm/ocaml/tactics/equalityTactics.mli		diff \| blob \| history
helm/ocaml/tactics/fourierR.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineHelpers.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineTypes.ml		diff \| blob \| history
helm/ocaml/tactics/proofEngineTypes.mli		diff \| blob \| history
helm/ocaml/tactics/reductionTactics.ml		diff \| blob \| history
helm/ocaml/tactics/reductionTactics.mli		diff \| blob \| history
helm/ocaml/tactics/tactics.mli		diff \| blob \| history
helm/ocaml/tactics/variousTactics.ml		diff \| blob \| history
helm/ocaml/tactics/variousTactics.mli		diff \| blob \| history

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