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

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

2004-02-06	Stefano Zacchiroli	added -g flag to ocamlc per default	commit \| commitdiff \| tree \| snapshot
2004-02-06	Stefano Zacchiroli	textual term editor is now the default one	commit \| commitdiff \| tree \| snapshot
2004-02-06	Stefano Zacchiroli	ignore .debug_script (used by Makefile's debug target)	commit \| commitdiff \| tree \| snapshot
2004-02-06	Stefano Zacchiroli	- split regtest/testlibrary/gTopLevel objects so that...	commit \| commitdiff \| tree \| snapshot
2004-02-06	Andrea Asperti	Bug MutCase fixed: now the type of the constructor...	commit \| commitdiff \| tree \| snapshot
2004-02-06	Stefano Zacchiroli	added testlibrary.opt and some cm****	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	NameExpected exception removed. The "identifier" __n...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	Improved error messages.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	No more garbage in the metasenv.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	New target librarytest (to apply testlibrary.opt to...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	- added support for multiple choices	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	better output format	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	flush stdout after print_string	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	debug prints on stderr	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	removed duplicated entry about freshNamesGenerator	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	- added testlibrary .opts	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	added \to notation for anonymous binders Pi and Lambda	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	bugfix: use rev_uniq also on non-located term	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	sort_of_prod relaxed to accept also Metas (when the...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	- sort_of_prod now returns the second Meta (if it is...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	added html_of_html_msg	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	__n no longer generated.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	"assert false" relaxed to a warning.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	No longer puts anonymous declarations in the canonical...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	- the result of a refinement is now cleared from dummy...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	freshNameGenerator.ml* added	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	rebuilt	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	added freshNameGenerator	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	added testlibrary script	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	use a dummy location when no location is provided	commit \| commitdiff \| tree \| snapshot
2004-02-05	Stefano Zacchiroli	added ( ) notation for binders	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	dummy dependent types and dummy letins are now removed...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	fresh_name_generator has now also the metasenv parameter.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	mk_fresh_name moved to FreshNamesGenerator.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	New test.	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	Final answer: the local context MUST be normalized...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	Restrict reimplemented to avoid generating lists of...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	Added a TODO (to catch only the right exceptions instea...	commit \| commitdiff \| tree \| snapshot
2004-02-05	Claudio Sacerdoti...	Bug fixed: the canonical contexts were traversed in...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Rel to hidden hypotheses are now printed as _hidden_n.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	ppterm_in_context exported	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	ppcontext (and thus also ppmetasenv) were buggy: the...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Functors must be applied using parentheses around the...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Added newline.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Bug fixed: restriction of already restricted contexts...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Effects of fixing bugs for other regression tests ;-)	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	We no longer apply the subst to a Meta in force_does_no...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Andrea Asperti	delift no longer apply the substitution when a Meta...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Andrea Asperti	Added a new example.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	report files are now produced (and removed) during...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Patch to delift withdrawn.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Typo fixed. Used to break target gentest.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Bug fixed: when a variable not instantiated yet was...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	Improved regression testing reporting.	commit \| commitdiff \| tree \| snapshot
2004-02-04	Claudio Sacerdoti...	- regtest: better argument handling (using Arg)	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	removed a debugging message	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	- improved some error messages	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	moved here CicAst and pretty printer	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	ported to CicAst	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	- sorted domain which hopefully avoids exponential...	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	moved Ast in cic_transformations/	commit \| commitdiff \| tree \| snapshot
2004-02-04	Stefano Zacchiroli	- added support for implicit in concrete syntax	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	regression tests	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	cic_mkimplicit' removed (its implementation was wrong...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	sort_of_prod changed to not generate a new metavariable...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	- comment inside .test file that explain what follows	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	added cleantest target (removes tests/*.test)	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	Check missed: the two metasenv were not compared.	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	Debuggin infos removed.	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	- do not crash any longer if type-checking or reduction...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	time added to regtest	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	catch just AssertFailure instead of _ (AssertFailure...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	removed SortExpectedMetaFound special exception	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	added urimanager dependency	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	Meta vs same Meta now tries unification when convertibi...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	s/LocatedTerm/AnnotatedTerm + various annotations/	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	New tests for lambdas (that show bugs in applications ;-)	commit \| commitdiff \| tree \| snapshot
2004-02-03	Stefano Zacchiroli	catch exceptions and mark corresponding tests as failed	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	eat_prods reimplemented to generalize the output type...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	Added an optional parameter to identity_relocation_list...	commit \| commitdiff \| tree \| snapshot
2004-02-03	Claudio Sacerdoti...	More debug informations.	commit \| commitdiff \| tree \| snapshot
2004-02-02	Claudio Sacerdoti...	Substitution no longer returned from CicRefine.type_of_aux	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	ported to new type_of prototype	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	uses CicMetaSubst.ppterm where needed	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- refine's type_of no longer return a substitution	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	ported to latest Ast changes (mainly capture_variable...	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- added entries for capture variables parsing	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- added capture_variable entry and Cic.names here and...	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- changed ast for pattern matching so that type annotat...	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- big hack: keep on unifying/refining when SortExpected...	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- removed metasenv argument from kernel proxies invocations	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- added SortExpectedMetaFound exception (huge hack)	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- bugfix for expand_implicits, return correct term...	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	- removed unwind: every substitution is now _not_ unwinded	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	changed prototype of CicMetaSubst.apply_subst*	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	added comments	commit \| commitdiff \| tree \| snapshot
2004-02-02	Stefano Zacchiroli	fact regtest	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom