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

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

2008-12-15	Wilmer Ricciotti	First attempt to implement unification hints.	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	use named types to force some constraints asap	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	To check if a term is type, do a whd of its sort before...	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-15	Enrico Tassi	aded some whd, you should be able to declare something...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Claudio Sacerdoti...	The library is no longer automatically used during...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	- improved logging	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	new kernel basic_ag (with absolute local references)	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	we are changing the kernel version from basic_rg to...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Ferruccio Guidi	autItem : the uris of the objects involved in the impli...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Enrico Tassi	eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg...	commit \| commitdiff \| tree \| snapshot
2008-12-14	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Ferruccio Guidi	improved type hierarchy management	commit \| commitdiff \| tree \| snapshot
2008-12-12	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Claudio Sacerdoti...	A parser (and a scanner) to import "~C" files into...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Claudio Sacerdoti...	1. new expressions AND, OR, XOR	commit \| commitdiff \| tree \| snapshot
2008-12-12	Ferruccio Guidi	- basic_rg: architectural bug fix	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	added some hardcoded universes, needed to typecheck...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	added some messages	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	added empty_db, usefull to avoid translating all old...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	use new function to clear caches so that objects are...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	better error message, functions to clear various caches...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	thanks to the new fixes to notation, I can define ...	commit \| commitdiff \| tree \| snapshot
2008-12-12	Enrico Tassi	pattern matching over Ast.Case simplified:	commit \| commitdiff \| tree \| snapshot
2008-12-11	Claudio Sacerdoti...	Applications are now processed from left to right.	commit \| commitdiff \| tree \| snapshot
2008-12-11	Enrico Tassi	support for mathml mpadded tag added (allows to overlap...	commit \| commitdiff \| tree \| snapshot
2008-12-10	Ferruccio Guidi	- new semantic log system	commit \| commitdiff \| tree \| snapshot
2008-12-09	Ferruccio Guidi	first version of kernel "basic_rg"	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	new disambiguatio attached with the right universe...	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	raise uncertain when a sort is not a sort but may be...	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	better coercions indexing and lookup	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	better max function (instead of @) for combining universes	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	added an exception	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	saturate was not returning the correct (saturated)...	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	fixed notation	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-09	Enrico Tassi	option to collapse all tex macros implemented	commit \| commitdiff \| tree \| snapshot
2008-12-08	Claudio Sacerdoti...	A (boring and long) once-in-a-life exercise on proving...	commit \| commitdiff \| tree \| snapshot
2008-12-08	Enrico Tassi	non active but almost working implementation of \TeX...	commit \| commitdiff \| tree \| snapshot
2008-12-08	Enrico Tassi	alt-l for not working nymore for \fox where x was in...	commit \| commitdiff \| tree \| snapshot
2008-12-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-08	Enrico Tassi	better replacement for \\def	commit \| commitdiff \| tree \| snapshot
2008-12-08	Enrico Tassi	3.5 -> 35 to help crappy latex	commit \| commitdiff \| tree \| snapshot
2008-12-07	Claudio Sacerdoti...	New exception considered.	commit \| commitdiff \| tree \| snapshot
2008-12-07	Claudio Sacerdoti...	Bug fixed: every time we form a Prod, we must typecheck...	commit \| commitdiff \| tree \| snapshot
2008-12-07	Enrico Tassi	better images	commit \| commitdiff \| tree \| snapshot
2008-12-06	Enrico Tassi	new concept of virtuals, defined only in the gui that...	commit \| commitdiff \| tree \| snapshot
2008-12-06	Ferruccio Guidi	metaAut: now we use hash tables properly (processing...	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	new exception captured	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Added new syntax Type[n] where n is a number.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Debugging code removed	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Debugging instructions removed.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Useless code removed.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Useless code removed.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Useless code removed.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Claudio Sacerdoti...	Case-sensitive fixes.	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	a few missing ~subst added to whd	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	coercions are there, but not heavily tested	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	if todo_dom was [] disambiguation was performed twice	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	still commented, but benchmarks the new/old disambiguti...	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	disambiguation takes ~mk_localization_tbl and not ...	commit \| commitdiff \| tree \| snapshot
2008-12-05	Enrico Tassi	raise failure instead of uncertain if two terms are...	commit \| commitdiff \| tree \| snapshot
2008-12-04	Enrico Tassi	Fixes:	commit \| commitdiff \| tree \| snapshot
2008-12-04	Enrico Tassi	housekeeping:	commit \| commitdiff \| tree \| snapshot
2008-12-04	Enrico Tassi	Bug fixed: pretty-printing of aliases when the OK butto...	commit \| commitdiff \| tree \| snapshot
2008-12-03	Claudio Sacerdoti...	The aliases and multi_aliases in the lexicon status...	commit \| commitdiff \| tree \| snapshot
2008-12-03	Ferruccio Guidi	improved interface for brgEnvironment	commit \| commitdiff \| tree \| snapshot
2008-12-03	Ferruccio Guidi	log facility, initial environment for basic_rg	commit \| commitdiff \| tree \| snapshot
2008-12-02	Ferruccio Guidi	- we updated some preambles to match that of nUri.ml	commit \| commitdiff \| tree \| snapshot
2008-12-02	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	0.5.6 almost ok	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	0.5.6	commit \| commitdiff \| tree \| snapshot
2008-12-01	Ferruccio Guidi	we start a kernel for the version "basic with reverse...	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	all done	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	more ex and more notation	commit \| commitdiff \| tree \| snapshot
2008-12-01	Enrico Tassi	better doc	commit \| commitdiff \| tree \| snapshot
2008-12-01	Claudio Sacerdoti...	rt.op and check.opt removed from Makefile	commit \| commitdiff \| tree \| snapshot
2008-11-30	Enrico Tassi	natural deduction support for lemmas with premises	commit \| commitdiff \| tree \| snapshot
2008-11-30	Ferruccio Guidi	lambda-delta/toplevel: improved transformation from...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Ferruccio Guidi	cicDischarge: final fixup. Now correctly processes...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Ferruccio Guidi	ng_disambiguation ng_kernel ng_refiner disambiguation...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	it works!	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	new disambiguator almost attached	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	\forall x:?. and \forall x. both generate a meta for...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	metas for terms have height 3	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	virtualbox guide almost ok	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-11-28	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2008-11-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-11-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-11-27	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2008-11-27	Enrico Tassi	New modules stack:	commit \| commitdiff \| tree \| snapshot
2008-11-27	Enrico Tassi	cic_disambiguation splitted into disambiguation and...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom