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

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

2004-02-05	Claudio Sacerdoti...	sort_of_prod relaxed to accept also Metas (when the...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	- sort_of_prod now returns the second Meta (if it is...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	__n no longer generated.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	"assert false" relaxed to a warning.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	No longer puts anonymous declarations in the canonical...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	- the result of a refinement is now cleared from dummy...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	freshNameGenerator.ml* added	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	dummy dependent types and dummy letins are now removed...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	fresh_name_generator has now also the metasenv parameter.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	mk_fresh_name moved to FreshNamesGenerator.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	New test.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	Final answer: the local context MUST be normalized...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	Restrict reimplemented to avoid generating lists of...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	Added a TODO (to catch only the right exceptions instead...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	Bug fixed: the canonical contexts were traversed in...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Rel to hidden hypotheses are now printed as _hidden_n.	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	ppterm_in_context exported	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	ppcontext (and thus also ppmetasenv) were buggy: the...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Functors must be applied using parentheses around the...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Added newline.	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Bug fixed: restriction of already restricted contexts...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Effects of fixing bugs for other regression tests ;-)	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	We no longer apply the subst to a Meta in force_does_not_occ...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	report files are now produced (and removed) during...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Patch to delift withdrawn.	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Typo fixed. Used to break target gentest.	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Bug fixed: when a variable not instantiated yet was...	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	Improved regression testing reporting.	commit \| commitdiff \| tree
2004-02-04	Claudio Sacerdoti...	- regtest: better argument handling (using Arg)	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	regression tests	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	cic_mkimplicit' removed (its implementation was wrong...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	sort_of_prod changed to not generate a new metavariable...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	Check missed: the two metasenv were not compared.	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	Debuggin infos removed.	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	- do not crash any longer if type-checking or reduction...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	time added to regtest	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	Meta vs same Meta now tries unification when convertibility...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	New tests for lambdas (that show bugs in applications ;-)	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	eat_prods reimplemented to generalize the output type...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	Added an optional parameter to identity_relocation_list...	commit \| commitdiff \| tree
2004-02-03	Claudio Sacerdoti...	More debug informations.	commit \| commitdiff \| tree
2004-02-02	Claudio Sacerdoti...	Substitution no longer returned from CicRefine.type_of_aux	commit \| commitdiff \| tree
2004-01-30	Claudio Sacerdoti...	Refinement of Fix and CoFix now implemented.	commit \| commitdiff \| tree
2004-01-29	Claudio Sacerdoti...	- lift added to CicMetaSubst	commit \| commitdiff \| tree
2004-01-26	Claudio Sacerdoti...	Generated ml files added.	commit \| commitdiff \| tree
2004-01-23	Claudio Sacerdoti...	Eureka!	commit \| commitdiff \| tree
2004-01-23	Claudio Sacerdoti...	- Added DisambiguatingParser (that abstracts both the...	commit \| commitdiff \| tree
2004-01-23	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2004-01-22	Claudio Sacerdoti...	The parser have been made more functional with a trick.	commit \| commitdiff \| tree
2004-01-22	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2004-01-20	Claudio Sacerdoti...	/projects/helm/log moved to /var/log/mowgli	commit \| commitdiff \| tree
2004-01-20	Claudio Sacerdoti...	/projects/helm/run/*_mowgli.pid moved into /var/run	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Scripts simplified (since now we have only one cluster...	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	NuPRL stuff moved.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	No longer in use. The official repository for the	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Branch V7_3_new_exportation merged.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Error message updated.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	No more in use.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	We are now using the standard dot distribution of debian.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Only V7_mowgli left.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Daemons moved to /projects/helm/daemons.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Daemon moved to /projects/helm/daemons.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	* empty log message *	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Several daemons moved into /projects/helm/daemons.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Errore message improved.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Missing package dependency.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Branch V7_3_new_exportation closed.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	mathql listed twice	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	The searchengine now requires the mathql_db_map.txt.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	No longer in use.	commit \| commitdiff \| tree
2004-01-19	Claudio Sacerdoti...	Error in the warning message.	commit \| commitdiff \| tree
2003-12-18	Claudio Sacerdoti...	Bug commented out. The comment is also commented.	commit \| commitdiff \| tree
2003-12-18	Claudio Sacerdoti...	Big bug spotted: restriction can fail and it was implicitly...	commit \| commitdiff \| tree
2003-12-18	Claudio Sacerdoti...	One of the bug I detected (and commented) in my last...	commit \| commitdiff \| tree
2003-12-17	Claudio Sacerdoti...	More comments. Some of them may highlight bugs or open...	commit \| commitdiff \| tree
2003-12-17	Claudio Sacerdoti...	Big bug spotted and commented: the delift function...	commit \| commitdiff \| tree
2003-12-17	Claudio Sacerdoti...	* comments improved an possible code weakness (i.e...	commit \| commitdiff \| tree
2003-12-17	Claudio Sacerdoti...	* Reindentation	commit \| commitdiff \| tree
2003-12-17	Claudio Sacerdoti...	* Reindentation.	commit \| commitdiff \| tree
2003-11-20	Claudio Sacerdoti...	The tmp is now cleared from the http___* files.	commit \| commitdiff \| tree
2003-11-07	Claudio Sacerdoti...	Porting to lablgtk2 completed.	commit \| commitdiff \| tree
2003-11-07	Claudio Sacerdoti...	The hbugs client interface is almost working again.	commit \| commitdiff \| tree
2003-11-06	Claudio Sacerdoti...	HBugs compile again (but it does not do anything right...	commit \| commitdiff \| tree
2003-11-06	Claudio Sacerdoti...	First release that compiles under lablgtk2 (but it...	commit \| commitdiff \| tree
2003-11-03	Claudio Sacerdoti...	* empty log message *	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	Reindentation.	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	ProofEngine.goal := ==> set_proof_engine_goal	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	Reindentation	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	ProofEngine.proof is now an abstract data type (since...	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	This version of xmlDiff is much much much smarter than...	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	Reindentation	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	BU_Conversion + omit-conclusion is a mess. I have partially...	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	Debugging stuff removed.	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	Preliminary support for proof-tree enhanced: proof...	commit \| commitdiff \| tree
2003-09-23	Claudio Sacerdoti...	- added support for proof trees	commit \| commitdiff \| tree
next

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

RSS Atom