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

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

2007-11-25	Claudio Sacerdoti...	This version of disambiguate.ml implements yet another...	commit \| commitdiff \| tree
2007-11-25	Claudio Sacerdoti...	Bug fixed: an unification exception used to escape...	commit \| commitdiff \| tree
2007-11-23	Claudio Sacerdoti...	This alternative version of disambiguate.crit2 implements...	commit \| commitdiff \| tree
2007-11-22	Claudio Sacerdoti...	Bug fixed in printing of passes in error messages.	commit \| commitdiff \| tree
2007-11-21	Claudio Sacerdoti...	Very incomplete example of simple calculus exercises...	commit \| commitdiff \| tree
2007-11-19	Claudio Sacerdoti...	Bug fixed: local type declarations are not allowed...	commit \| commitdiff \| tree
2007-11-18	Claudio Sacerdoti...	The axiom can be proved. Just follow the hint.	commit \| commitdiff \| tree
2007-11-16	Claudio Sacerdoti...	Some notes for Enrico.	commit \| commitdiff \| tree
2007-11-14	Claudio Sacerdoti...	Bug fixed: yet another case where tys of mutual recursive...	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	a) Detection of existential types now implemented	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	More correct (but still bugged) implementation of type...	commit \| commitdiff \| tree
2007-11-10	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Trivial bug fixed in type inference of LetIn source...	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Arguments of constructors in a case pattern are now...	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	svn:ignore set	commit \| commitdiff \| tree
2007-11-08	Claudio Sacerdoti...	Zoli's note (in Italian) about a constructive version...	commit \| commitdiff \| tree
2007-11-06	Claudio Sacerdoti...	cic_acic should be compiled before cic_exportation	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Bug in detection of too polymorphic types partially...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	MutCases that occur in types should be handled with...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Obj.magic are now generated to extract dependently...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Handling of left parameters of constructors/indutive...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Slightly nicer output.	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Filenames are now fully mangled (e.g. matita_nat_nat...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	Type application and abstractions are now exported...	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	New OCaml keyword "val".	commit \| commitdiff \| tree
2007-11-05	Claudio Sacerdoti...	"f" => "aux" to avoid name clashes	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	The type parameters in an inductive type declaration...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Type arguments are better uncapitalized.	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Empty types not in Prop and empty types elimination...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Empty and singleton type elimination are now handled...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	1. type definitions of propositions are no longer exported...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	Bug fixed: qualified names were not generated correctly...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	* type definitions that define a new proposition are...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	CicExportation branched. Change "if false" with "if...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	All exported names are now qualified. This avoids the...	commit \| commitdiff \| tree
2007-11-04	Claudio Sacerdoti...	All names are now qualified. This avoids the need for...	commit \| commitdiff \| tree
2007-11-02	Claudio Sacerdoti...	* Very experimental and not branched *	commit \| commitdiff \| tree
2007-11-02	Claudio Sacerdoti...	Added an hook useful in many situations.	commit \| commitdiff \| tree
2007-10-31	Claudio Sacerdoti...	New image from Tassi's PhD thesis.	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	Bug fixed: patterns in hypotheses under binders where...	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	New syntax for match patterns in terms and in patterns.	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	The document was not valid. Fixed.	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	Pretty-printing of "match ... with" pattern syntax...	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	Nil => nil, Cons => cons	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	Nil => nil; Cons => cons	commit \| commitdiff \| tree
2007-10-28	Claudio Sacerdoti...	New syntax for match patterns.	commit \| commitdiff \| tree
2007-10-26	Claudio Sacerdoti...	Syntax of patterns changed (and not documented yet).	commit \| commitdiff \| tree
2007-10-26	Claudio Sacerdoti...	Wildcard patterns implemented in case analysis. The...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	neg => Qneg :-)	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	true and false were swapped!	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	flase => false :-)	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	Ooops. In previous commit I forgot to subtract the...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	Bug fixed: case analysis where a case had not the expected...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	Bug fixed: a MutCase considering a wrong number of...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	Bug fixed: a MutCase with missing or exceeding cases...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	1. More localization: interpretation errors are now...	commit \| commitdiff \| tree
2007-10-25	Claudio Sacerdoti...	Recently introduced bug fixed: error localization was...	commit \| commitdiff \| tree
2007-10-24	Claudio Sacerdoti...	Debugging code improved.	commit \| commitdiff \| tree
2007-10-16	Claudio Sacerdoti...	Interesting. Do we need many more inversion lemmas...	commit \| commitdiff \| tree
2007-10-16	Claudio Sacerdoti...	DOS-style CR+LF added to the blanks list.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Dead code clean-up.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	The behaviour of autobatch paramodulation has changed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Wrong test patched.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	discriminate.ma => destruct.ma	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Spurious code removed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Old wrong code to avoid old bug fixed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto ==> autobatch	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed (I deleted "assumption a" by error).	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree
2007-10-14	Claudio Sacerdoti...	Caseness problems fixed.	commit \| commitdiff \| tree
2007-10-14	Claudio Sacerdoti...	Some lemmas moves to the file they belong to.	commit \| commitdiff \| tree
2007-10-12	Claudio Sacerdoti...	Move to OCaml 3.10. Requires debian packages from unstable...	commit \| commitdiff \| tree
2007-10-11	Claudio Sacerdoti...	Old inversion bug fixed: it used to work only on the...	commit \| commitdiff \| tree
2007-09-13	Claudio Sacerdoti...	added a debug print	commit \| commitdiff \| tree
2007-09-10	Claudio Sacerdoti...	This test shows one of the few cases were Matita is...	commit \| commitdiff \| tree
2007-09-05	Claudio Sacerdoti...	added fix case	commit \| commitdiff \| tree
2007-09-05	Claudio Sacerdoti...	coercions are propagated under Fix (but not mutually...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	Dandling ")" removed from notation for 'exists.	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	Composition of coercions with arity > 0 is now implemented...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	A test for propagation of coercions (that open new...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	1. composition of coercions with saturations > 0 is...	commit \| commitdiff \| tree
2007-08-31	Claudio Sacerdoti...	alpha conversion to avoid case-insensitivity of MySql...	commit \| commitdiff \| tree
2007-08-31	Claudio Sacerdoti...	baseuri changed	commit \| commitdiff \| tree
2007-08-30	Claudio Sacerdoti...	Coercions are now generalized to the general form	commit \| commitdiff \| tree
2007-08-28	Claudio Sacerdoti...	* definition of implication free propositional formulas	commit \| commitdiff \| tree
2007-08-28	Claudio Sacerdoti...	A primer for Matita with some easy, medium, difficult...	commit \| commitdiff \| tree
2007-08-25	Claudio Sacerdoti...	thread-based interface activated again	commit \| commitdiff \| tree
2007-08-23	Claudio Sacerdoti...	Bug fixed: RewriteLR were not recognized correctly...	commit \| commitdiff \| tree
2007-08-23	Claudio Sacerdoti...	Bug fixed: the initial metasenv used in the two tactic...	commit \| commitdiff \| tree
2007-08-22	Claudio Sacerdoti...	Avoid reusing Hbeta several times.	commit \| commitdiff \| tree
2007-08-22	Claudio Sacerdoti...	select now works correctly even if multiple hypotheses...	commit \| commitdiff \| tree
2007-08-21	Claudio Sacerdoti...	Avoid confusion for names of proofs put in the applicative...	commit \| commitdiff \| tree
2007-08-21	Claudio Sacerdoti...	"obtain H E1=E2 by proof" is now working	commit \| commitdiff \| tree
next

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

RSS Atom