matita.cs.unibo.it Git - helm.git/history - matita/components/grafite

]> matita.cs.unibo.it Git - helm.git/history - matita/components/grafite_parser/grafiteParser.ml

[helm.git] / matita / components / grafite_parser / grafiteParser.ml

2018-08-01	Ferruccio Guidi	parameter sintax added to axiom statement	blob \| commitdiff \| raw
2016-04-18	Ferruccio Guidi	As required by M. Maietti,	blob \| commitdiff \| raw \| diff to current
2016-03-28	Ferruccio Guidi	minor correction on "source" production	blob \| commitdiff \| raw \| diff to current
2016-03-13	Ferruccio Guidi	- new syntax for let rec/corec with flavor specifier...	blob \| commitdiff \| raw \| diff to current
2016-01-26	Ferruccio Guidi	lexicon commands must tbe parsed before grafite command...	blob \| commitdiff \| raw \| diff to current
2015-09-23	Ferruccio Guidi	optional parameters added to the syntax of definitions,	blob \| commitdiff \| raw \| diff to current
2015-09-05	Ferruccio Guidi	- New attribute `Implied put beside `Generated and...	blob \| commitdiff \| raw \| diff to current
2015-01-30	Ferruccio Guidi	notation ast updated to comply with the toplevel let...	blob \| commitdiff \| raw \| diff to current
2014-10-19	Ferruccio Guidi	- grafiteParser: we added the comand "defined" as a...	blob \| commitdiff \| raw \| diff to current
2013-02-01	Ferruccio Guidi	- ng_refiner:	blob \| commitdiff \| raw \| diff to current
2012-10-19	Claudio Sacerdoti...	One useless Obj.magic removed.	blob \| commitdiff \| raw \| diff to current
2012-06-11	Claudio Sacerdoti...	New nohyps option for /demod/	blob \| commitdiff \| raw \| diff to current
2012-03-06	Claudio Sacerdoti...	Forward compatibility with new releases of Camlp5.	blob \| commitdiff \| raw \| diff to current
2011-12-13	Enrico Tassi	axiom-	blob \| commitdiff \| raw \| diff to current
2011-12-12	Enrico Tassi	support -axiom to avoind indexing an axiom (since there...	blob \| commitdiff \| raw \| diff to current
2011-12-06	Wilmer Ricciotti	Grammar change: let corecs can take no arguments (and...	blob \| commitdiff \| raw \| diff to current
2011-11-21	Claudio Sacerdoti...	Syntax change: change where what => change what where.	blob \| commitdiff \| raw \| diff to current
2011-11-21	Claudio Sacerdoti...	{pattern} => in pattern;	blob \| commitdiff \| raw \| diff to current
2011-11-18	Enrico Tassi	short notation for "coercion"	blob \| commitdiff \| raw \| diff to current
2011-11-18	Claudio Sacerdoti...	No longer used parameters of auto removed.	blob \| commitdiff \| raw \| diff to current
2011-11-18	Claudio Sacerdoti...	/by {}/ ==> /by/	blob \| commitdiff \| raw \| diff to current
2011-11-18	Claudio Sacerdoti...	* Almost ready for release 0.99.1.	blob \| commitdiff \| raw \| diff to current
2011-10-21	Andrea Asperti	Now it should compile :-)	blob \| commitdiff \| raw \| diff to current
2011-10-21	Andrea Asperti	Disabled debug.	blob \| commitdiff \| raw \| diff to current
2011-10-20	Andrea Asperti	QED takes a boolean parameter governing indexing.	blob \| commitdiff \| raw \| diff to current
2011-05-26	Claudio Sacerdoti...	Syntax for coercion nocomposites fixed.	blob \| commitdiff \| raw \| diff to current
2011-05-26	Claudio Sacerdoti...	Added "nocomposites" to coercions.	blob \| commitdiff \| raw \| diff to current
2011-03-22	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw \| diff to current
2011-03-19	Claudio Sacerdoti...	Bug "fixed" (i.e avoided).	blob \| commitdiff \| raw \| diff to current
2011-01-11	Claudio Sacerdoti...	HUGE COMMIT:	blob \| commitdiff \| raw \| diff to current
2010-12-10	Claudio Sacerdoti...	Previous patch improved: we now use an ad-hoc wrapper...	blob \| commitdiff \| raw \| diff to current
2010-12-10	Claudio Sacerdoti...	BIG BUG FIXED (???): in place of using Grammar.Entry...	blob \| commitdiff \| raw \| diff to current
2010-12-10	Andrea Asperti	Big change:	blob \| commitdiff \| raw \| diff to current
2010-12-10	Andrea Asperti	New syntax -H1 .. Hn for clear	blob \| commitdiff \| raw \| diff to current
2010-11-11	Andrea Asperti	let and let rec used wrong tokens	blob \| commitdiff \| raw \| diff to current
2010-11-05	Andrea Asperti	- cleanup	blob \| commitdiff \| raw \| diff to current
2010-11-05	Andrea Asperti	dead code removal: the parser used to be able to return...	blob \| commitdiff \| raw \| diff to current
2010-11-04	Claudio Sacerdoti...	- further simplifications (??) of the status dependencies	blob \| commitdiff \| raw \| diff to current
2010-11-04	Claudio Sacerdoti...	dependencies between statuses simplified	blob \| commitdiff \| raw \| diff to current
2010-11-03	Enrico Tassi	notation kind of works	blob \| commitdiff \| raw \| diff to current
2010-11-03	Andrea Asperti	- LexiconAst merged into GrafiteAst	blob \| commitdiff \| raw \| diff to current
2010-11-02	Enrico Tassi	big change in parsing, trying to make all functional	blob \| commitdiff \| raw \| diff to current
2010-10-29	Andrea Asperti	- grammar of // changed to move the justification inside;	blob \| commitdiff \| raw \| diff to current
2010-10-26	Andrea Asperti	urimanager removed	blob \| commitdiff \| raw \| diff to current
2010-10-26	Andrea Asperti	cic module removed (RIP)	blob \| commitdiff \| raw \| diff to current
2010-10-22	Enrico Tassi	tentative parser patch with symbolic tactics names	blob \| commitdiff \| raw \| diff to current
2010-10-15	Claudio Sacerdoti...	- bug fixed (introduced by last commit from Andrea...	blob \| commitdiff \| raw \| diff to current
2010-10-13	Andrea Asperti	Propagation of changes to grafiteAst.	blob \| commitdiff \| raw \| diff to current
2010-10-08	Andrea Asperti	Cic.term and Cic.obj unused!	blob \| commitdiff \| raw \| diff to current
2010-10-08	Andrea Asperti	cicNotation* ==> notation*	blob \| commitdiff \| raw \| diff to current
2010-10-06	Andrea Asperti	nAuto --> nnAuto	blob \| commitdiff \| raw \| diff to current
2010-10-05	Andrea Asperti	- parser: "whelp ...Â"removed	blob \| commitdiff \| raw \| diff to current
2010-09-30	Claudio Sacerdoti...	Stuff moved from old Matita.	blob \| commitdiff \| raw \| diff to current

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

RSS Atom