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

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

2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	test/a.ma => tests/ng_tactics.ma, with nassert here...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	Replaced long, bugged implementation of letin-tac with...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	Added ppterm.	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	The context is now parsed in the reverse (right) order.	commit \| commitdiff \| tree \| snapshot
2009-04-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-16	Enrico Tassi	Universe is used only locally to tactics/	commit \| commitdiff \| tree \| snapshot
2009-04-16	Enrico Tassi	added an exception	commit \| commitdiff \| tree \| snapshot
2009-04-15	Ferruccio Guidi	- transcript: bugfix	commit \| commitdiff \| tree \| snapshot
2009-04-14	Ferruccio Guidi	we rebuilt the dependences	commit \| commitdiff \| tree \| snapshot
2009-04-14	Ferruccio Guidi	- Procedural: generation of "exact" is now complete	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	Trick: the refiner always subst-expands the outtype...	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	Bug fixed in two lines + 5 lines of comment.	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	assert_tac now takes a list of sequents and also checks...	commit \| commitdiff \| tree \| snapshot
2009-04-14	Claudio Sacerdoti...	New debugging tactic nassert:	commit \| commitdiff \| tree \| snapshot
2009-04-12	Claudio Sacerdoti...	Semantic selection back again (but no semantic cut...	commit \| commitdiff \| tree \| snapshot
2009-04-12	Claudio Sacerdoti...	Match is now rendered as best as possible.	commit \| commitdiff \| tree \| snapshot
2009-04-10	Claudio Sacerdoti...	The sequent viewer now considers the context to render...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Ferruccio Guidi	- character: we adjusted some "autobatch" parameters	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	The substitution is now taken in account when printing...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	added letin, still broken	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	new tactic whd implemented	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	- change implemented in 4 lines	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	- generalize finished	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	?_OS1 := C[ ?_IN ]	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	fixed modules order	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	minor fixes	commit \| commitdiff \| tree \| snapshot
2009-04-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-09	Claudio Sacerdoti...	+ Chain NCic.term -> content -> presentation very...	commit \| commitdiff \| tree \| snapshot
2009-04-08	Claudio Sacerdoti...	Just to make it compile again.	commit \| commitdiff \| tree \| snapshot
2009-04-08	Enrico Tassi	generalized is half-implemented (still broken)	commit \| commitdiff \| tree \| snapshot
2009-04-08	Enrico Tassi	Analizyng the inductive type of the eliminated term and	commit \| commitdiff \| tree \| snapshot
2009-04-07	Claudio Sacerdoti...	- nrewrite ((very?) rough implementation)	commit \| commitdiff \| tree \| snapshot
2009-04-07	Claudio Sacerdoti...	- more progress towards generalize, but I am stuck now	commit \| commitdiff \| tree \| snapshot
2009-04-07	Enrico Tassi	- select_tac honors the hypotheses pattern when require...	commit \| commitdiff \| tree \| snapshot
2009-04-07	Enrico Tassi	select honors the substitution	commit \| commitdiff \| tree \| snapshot
2009-04-06	Claudio Sacerdoti...	New tactic clear; new syntax # _; to introduce and...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	tactic cases works! delift clears tags	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	eta-contraction was made on the wrong term	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	unification:	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	better error message	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	added one exception	commit \| commitdiff \| tree \| snapshot
2009-04-06	Ferruccio Guidi	- external quantification removed (will be reintroduced...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Ferruccio Guidi	limits: reorganized and attached to nightly tests ...	commit \| commitdiff \| tree \| snapshot
2009-04-06	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2009-04-05	Ferruccio Guidi	- Procedural: now we generate the exact tactic (in...	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	New file nTacStatus to:	commit \| commitdiff \| tree \| snapshot
2009-04-02	Enrico Tassi	added analyse_indty	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	New tactic "case1_tac" that make "intro" followed by...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	## prefix is now used for tinycals	commit \| commitdiff \| tree \| snapshot
2009-04-01	Claudio Sacerdoti...	New tactic intro. Syntax: "# n".	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	added tentative elim	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	1) mk_meta now returns also the index of the created...	commit \| commitdiff \| tree \| snapshot
2009-04-01	Enrico Tassi	removed spurious "	commit \| commitdiff \| tree \| snapshot
2009-03-30	Enrico Tassi	tentative subst-sexpand and change	commit \| commitdiff \| tree \| snapshot
2009-03-30	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-27	Enrico Tassi	more comments	commit \| commitdiff \| tree \| snapshot
2009-03-27	Enrico Tassi	exec and distribute implemented	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	new apply almost there	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-26	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-25	Enrico Tassi	new tactics are almost ready	commit \| commitdiff \| tree \| snapshot
2009-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	add Homepage field	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	set package section to "ocaml"	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	add missing ${misc:Depends}, thanks lintian!	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	release to unstable	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	debian/*.in: more abstract substvars	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	debian/rules: use ocaml.mk as a CDBS "rules" snippet	commit \| commitdiff \| tree \| snapshot
2009-03-19	Stefano Zacchiroli	refresh build-dependencies for the transition	commit \| commitdiff \| tree \| snapshot
2009-03-16	Enrico Tassi	added mactions, the three can now be collapsed to fit...	commit \| commitdiff \| tree \| snapshot
2009-03-16	Andrea Asperti	New parameters for applyS: 10 20.	commit \| commitdiff \| tree \| snapshot
2009-03-16	Andrea Asperti	Adapted to new applyS.	commit \| commitdiff \| tree \| snapshot
2009-03-16	Andrea Asperti	Added a property.	commit \| commitdiff \| tree \| snapshot
2009-03-12	Claudio Sacerdoti...	More details on the proof.	commit \| commitdiff \| tree \| snapshot
2009-03-12	Claudio Sacerdoti...	New algorithm based on in-place modification of the...	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	matitacLib: Gc.compact added after the compilation...	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	Procedural: id tactics are not counted, ie they are...	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	bug fix + better obj flavour guessing via inner sorts	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	the level 1 reconstruction procedure is now in Procedural1	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	....	commit \| commitdiff \| tree \| snapshot
2009-03-11	Ferruccio Guidi	new dependences	commit \| commitdiff \| tree \| snapshot
2009-03-11	Enrico Tassi	unification hints with recursive calls do work!	commit \| commitdiff \| tree \| snapshot
2009-03-11	Enrico Tassi	added margin option to the pp	commit \| commitdiff \| tree \| snapshot
2009-03-11	Enrico Tassi	more examples	commit \| commitdiff \| tree \| snapshot
2009-03-10	Enrico Tassi	unificatiom hints with premises	commit \| commitdiff \| tree \| snapshot
2009-03-10	Ferruccio Guidi	added some commented debugging instructions :)	commit \| commitdiff \| tree \| snapshot
2009-03-10	Enrico Tassi	unification hints almost ready	commit \| commitdiff \| tree \| snapshot
2009-03-10	Enrico Tassi	notation ++	commit \| commitdiff \| tree \| snapshot
2009-03-10	Andrea Asperti	A version of applyS with bounded iterations of given_cl...	commit \| commitdiff \| tree \| snapshot
2009-03-10	Andrea Asperti	Removed the context from the metasenv to avoid trivial...	commit \| commitdiff \| tree \| snapshot
2009-03-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-03-06	Claudio Sacerdoti...	Minor improvements in pretty-printing.	commit \| commitdiff \| tree \| snapshot
2009-03-05	Claudio Sacerdoti...	New version: only new nodes are normalized; moreover...	commit \| commitdiff \| tree \| snapshot
2009-03-03	Enrico Tassi	- fixed hint generation, more hints are generated	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom