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

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

2008-07-12	Claudio Sacerdoti...	New feature/bug fixed (hopefully): it is now possible...	commit \| commitdiff \| tree
2008-07-12	Claudio Sacerdoti...	Notation for existential partially fixed: it is now...	commit \| commitdiff \| tree
2008-07-11	Claudio Sacerdoti...	A very nice experiment using notation: we define the...	commit \| commitdiff \| tree
2008-07-11	Claudio Sacerdoti...	Exists is no longer an ad-hoc notation hard-coded in...	commit \| commitdiff \| tree
2008-07-11	Claudio Sacerdoti...	Added new ternary layout \infrule premises conclusion...	commit \| commitdiff \| tree
2008-07-04	Claudio Sacerdoti...	More definitions, following Ciraulo's Phd Thesis "Constructi...	commit \| commitdiff \| tree
2008-07-04	Claudio Sacerdoti...	Compatibility finished.	commit \| commitdiff \| tree
2008-07-04	Claudio Sacerdoti...	Nice: cotransitivity proved.	commit \| commitdiff \| tree
2008-07-03	Claudio Sacerdoti...	More work.	commit \| commitdiff \| tree
2008-07-03	Claudio Sacerdoti...	First few lemmas. But I have some problems in making...	commit \| commitdiff \| tree
2008-07-03	Claudio Sacerdoti...	First experiment in Padua about formal topologies.	commit \| commitdiff \| tree
2008-06-20	Claudio Sacerdoti...	Fixed bugs in the documentation of notation.	commit \| commitdiff \| tree
2008-06-20	Claudio Sacerdoti...	More documentation for notation.	commit \| commitdiff \| tree
2008-06-20	Claudio Sacerdoti...	Further documentation for notation.	commit \| commitdiff \| tree
2008-06-20	Claudio Sacerdoti...	- partial implementation of pattern for case documented	commit \| commitdiff \| tree
2008-06-19	Claudio Sacerdoti...	1. bug fixed in generalize_pattern: a lazy const_tac...	commit \| commitdiff \| tree
2008-06-19	Claudio Sacerdoti...	- notation fixed according to the new stricter semantics	commit \| commitdiff \| tree
2008-06-18	Claudio Sacerdoti...	interpretation documented	commit \| commitdiff \| tree
2008-06-13	Claudio Sacerdoti...	New lemma	commit \| commitdiff \| tree
2008-06-11	Claudio Sacerdoti...	New, much faster implementation of factorize.	commit \| commitdiff \| tree
2008-06-09	Claudio Sacerdoti...	Most of the time, URIs can now be replaced with identifiers...	commit \| commitdiff \| tree
2008-06-09	Claudio Sacerdoti...	It is now possible to use identifiers in place of URI...	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required by elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	Generalize no more required for elim.	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more required before elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	generalize no more useful for elim	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	Bug fixed: wrong default pattern for generalize.	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	New: pattern for elim documented.	commit \| commitdiff \| tree
2008-06-08	Claudio Sacerdoti...	Hypotheses patterns for elim implemented. No more need...	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	Even more Q stuff moved around.	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	Even more Q stuff classified.	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	more stuff moved around	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	More Q stuff organized in a coherent way.	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	First snapshot at trying to clean up the Q library.	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	sieve.ma now depends only on primes.ma	commit \| commitdiff \| tree
2008-06-06	Claudio Sacerdoti...	Reduce reduction tactic got rid of a long time ago.	commit \| commitdiff \| tree
2008-06-05	Claudio Sacerdoti...	Eratosthene's sieve factorized out of nat/bertrand...	commit \| commitdiff \| tree
2008-06-03	Claudio Sacerdoti...	Some proofs on enumerator and denominator.	commit \| commitdiff \| tree
2008-06-03	Claudio Sacerdoti...	More work on rational numbers with unique representations.	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	Here is where we should add relevance checks.	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	Bug fixed in computation of leftnos: variables were...	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	Code simplification.	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	Added cprop <= type constraint.	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	We do not need to give cprop a special status yet.	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	CProp dropped in favour of a cprop universe exported...	commit \| commitdiff \| tree
2008-05-19	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Bug fixed: when computing the left arguments, I was...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	New missing check implemented: the left parameters...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent types are no longer cleaned in inductive...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Dummy dependent products in inductive types arities...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	This commit avoids cleaning dummy dependent types in...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Implemented translation of inductive types from the...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Serious bug fixed: the max of two universes was computed...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Synch with the paper.	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree
2008-05-18	Claudio Sacerdoti...	More effective optimization: avoid introducing already...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	New check implemented: the sort of each constructor...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	Missing check implemented: the sort of each constructors...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	The file bug_universi.ma shows a strage case where...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	Missing whd.	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	Bug fixed: since circular <= graphs are allowed, added...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	Bug fixed: only Type < Type1 was declared.	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	Bug fixed and further code semplification in management...	commit \| commitdiff \| tree
2008-05-17	Claudio Sacerdoti...	The code for universes was not correct in many borderline...	commit \| commitdiff \| tree
2008-05-15	Claudio Sacerdoti...	Timings	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	list_iter2_default_value moved to HExtlib. 1 euro to...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	eat_lambdas and eat_or_subst_lambdas taken out of the...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	debruijn simplified. It could go in nCicUtils, but...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	Bug fixed: types were check for conversion in the wrong...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	We forgot an important check: the declared and expected...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	New checks for well-formedness of metasenvs and substs.	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_refer...	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	Nicer graph.	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	map_hash moved to HExtlib	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	New function map_hash.	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	Generation of dot file.	commit \| commitdiff \| tree
2008-05-14	Claudio Sacerdoti...	New licence used uniformly everywhere.	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	One more bug fixed: we tried to perform List.nth on...	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	More exceptions captured.	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	Bug fixed in pretty-printing of free Rels.	commit \| commitdiff \| tree
next

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

RSS Atom