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

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

2004-02-11	Claudio Sacerdoti...	added target *.opt (e.g. test.opt, librarytest.opt...	commit \| commitdiff \| tree
2004-02-11	Claudio Sacerdoti...	- make *opt fixed	commit \| commitdiff \| tree
2004-02-11	Claudio Sacerdoti...	Big changes:	commit \| commitdiff \| tree
2004-02-11	Claudio Sacerdoti...	Added copyright notice.	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	Explicit Named Substitutions now supported.	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	CicCache ==> CicEnvironment (in testlibrary.ml)	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	- fixed final log reporting (that was broken by one...	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	Bug fixed: when an axiom was asked, an exception was...	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	Only applications whose head was a constant were eta...	commit \| commitdiff \| tree
2004-02-10	Claudio Sacerdoti...	Bug fixed: checking inductive type declarations with...	commit \| commitdiff \| tree
2004-02-09	Claudio Sacerdoti...	Added flag ?eta_fix:bool to acic_object_of_cic_object.	commit \| commitdiff \| tree
2004-02-09	Claudio Sacerdoti...	sort_of_prod now thinks that a "sort metavariable"...	commit \| commitdiff \| tree
2004-02-09	Claudio Sacerdoti...	Added is_closed.	commit \| commitdiff \| tree
2004-02-09	Claudio Sacerdoti...	eat_prods now uses mk_implicit_type.	commit \| commitdiff \| tree
2004-02-07	Claudio Sacerdoti...	- Added mk_implicit_sort.	commit \| commitdiff \| tree
2004-02-07	Claudio Sacerdoti...	Added mk_implicit_sort.	commit \| commitdiff \| tree
2004-02-07	Claudio Sacerdoti...	A better (but yet not empty) metasenv is now returned.	commit \| commitdiff \| tree
2004-02-07	Claudio Sacerdoti...	sort_of_prod: the second term, when it is a meta, was...	commit \| commitdiff \| tree
2004-02-06	Claudio Sacerdoti...	sort metavariables are now generated in an empty canonical...	commit \| commitdiff \| tree
2004-02-06	Claudio Sacerdoti...	Comments (notes) removed.	commit \| commitdiff \| tree
2004-02-06	Claudio Sacerdoti...	Code riorganization.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	NameExpected exception removed. The "identifier" __n...	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	Improved error messages.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	No more garbage in the metasenv.	commit \| commitdiff \| tree
2004-02-05	Claudio Sacerdoti...	New target librarytest (to apply testlibrary.opt to...	commit \| commitdiff \| tree
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
next

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

RSS Atom