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

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

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
2008-05-13	Claudio Sacerdoti...	Never commit before trying to compile... stupid typo...	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	Used old kernel exception in place of brand new one.	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	- is_closed removed from the kernel (it used to make...	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	Library factorized out.	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	Type of conjecture and subst_entry made uniform.	commit \| commitdiff \| tree
2008-05-13	Claudio Sacerdoti...	Added boolean "is_inductive" to NReference.Ind	commit \| commitdiff \| tree
2008-05-12	Claudio Sacerdoti...	trust is always false by default	commit \| commitdiff \| tree
2008-05-12	Claudio Sacerdoti...	trust implemented, but in the nCicTypeChecker!	commit \| commitdiff \| tree
2008-05-12	Claudio Sacerdoti...	New implementation of CicEnvironment:	commit \| commitdiff \| tree
2008-05-09	Claudio Sacerdoti...	Bug fixed: the domain of a LetRec was only made by...	commit \| commitdiff \| tree
2008-05-07	Claudio Sacerdoti...	Update after some more bug fixing.	commit \| commitdiff \| tree
2008-05-07	Claudio Sacerdoti...	Partially reverted bad merge by Enrico that re-introduced...	commit \| commitdiff \| tree
2008-05-05	Claudio Sacerdoti...	More bugs fixed.	commit \| commitdiff \| tree
2008-05-03	Claudio Sacerdoti...	Bug fixed in handling of explicit named substitutions...	commit \| commitdiff \| tree
2008-05-03	Claudio Sacerdoti...	Broken XML files either fixed or removed.	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	More precise classification of failures.	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	List of all URIS comprising:	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	More options can now be set at the beginning of the...	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	Last (???) bug about variables with bodies fixed: we...	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	Another case where the presence of variables with bodies...	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	Bug fixed: application without arguments generated...	commit \| commitdiff \| tree
2008-05-01	Claudio Sacerdoti...	New bug found.	commit \| commitdiff \| tree
2008-04-30	Claudio Sacerdoti...	Things are getting better.	commit \| commitdiff \| tree
2008-04-30	Claudio Sacerdoti...	Implementation of guarded_by_destructor is now complete...	commit \| commitdiff \| tree
2008-04-30	Claudio Sacerdoti...	Reducing an open term should not be an error (or should...	commit \| commitdiff \| tree
2008-04-30	Claudio Sacerdoti...	stupid error fixed	commit \| commitdiff \| tree
2008-04-30	Claudio Sacerdoti...	fixed_args fixed to accept passing a partially applied...	commit \| commitdiff \| tree
2008-04-29	Claudio Sacerdoti...	Tests status update.	commit \| commitdiff \| tree
2008-04-28	Claudio Sacerdoti...	Avoid (whd ~delta:true) during guarded_by_destructors...	commit \| commitdiff \| tree
2008-04-28	Claudio Sacerdoti...	In guarded by destructors, avoid computing the (whd...	commit \| commitdiff \| tree
2008-04-24	Claudio Sacerdoti...	Update...	commit \| commitdiff \| tree
2008-04-24	Claudio Sacerdoti...	No more bugs on guarded_by_constructors in the old...	commit \| commitdiff \| tree
2008-04-24	Claudio Sacerdoti...	When going under a binder, a term must be converted...	commit \| commitdiff \| tree
2008-04-24	Claudio Sacerdoti...	Working and broken URIs.	commit \| commitdiff \| tree
2008-04-23	Claudio Sacerdoti...	Avoid other comparisons on universes using =.	commit \| commitdiff \| tree
2008-04-23	Claudio Sacerdoti...	Avoid code duplication.	commit \| commitdiff \| tree
2008-04-23	Claudio Sacerdoti...	Do NOT dare using Pervasives.compare on data structures...	commit \| commitdiff \| tree
2008-04-22	Claudio Sacerdoti...	Types for LetIns computed during parsing for Coq objects...	commit \| commitdiff \| tree
2008-04-21	Claudio Sacerdoti...	defn2.ma is to be used with part1a_inversion3	commit \| commitdiff \| tree
2008-04-20	Claudio Sacerdoti...	Alternative prove using just one induction/inversion...	commit \| commitdiff \| tree
2008-04-19	Claudio Sacerdoti...	oblivion_ugraph => empty_ugraph	commit \| commitdiff \| tree
2008-04-19	Claudio Sacerdoti...	Added to flags to activate/disactivate pretty-printing...	commit \| commitdiff \| tree
2008-04-19	Claudio Sacerdoti...	Uris must be stripped of their xpointers.	commit \| commitdiff \| tree
2008-04-18	Claudio Sacerdoti...	Dead code removed.	commit \| commitdiff \| tree
2008-04-18	Claudio Sacerdoti...	Inversion lemma for Forall.	commit \| commitdiff \| tree
2008-04-15	Claudio Sacerdoti...	check_is_really_smaller simplified to consider that...	commit \| commitdiff \| tree
2008-04-15	Claudio Sacerdoti...	1. bug fixed: the context must be type-checked before...	commit \| commitdiff \| tree
2008-04-15	Claudio Sacerdoti...	added sample of guarded by in which coq is stronger	commit \| commitdiff \| tree
2008-04-11	Claudio Sacerdoti...	Extracted code. The main executable is medium_tests...	commit \| commitdiff \| tree
2008-04-10	Claudio Sacerdoti...	The cache of objects is now used also for cofixpoints.	commit \| commitdiff \| tree
2008-04-10	Claudio Sacerdoti...	New: cache of translated fixpoints (to avoid the generative...	commit \| commitdiff \| tree
2008-04-10	Claudio Sacerdoti...	does_not_occur exported to be used in oCic2NCic	commit \| commitdiff \| tree
2008-04-09	Claudio Sacerdoti...	Bug fixed: references to CoFix are CoFix, not Fix.	commit \| commitdiff \| tree
2008-04-09	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-04-09	Claudio Sacerdoti...	Fixed serious bug that occurred only in the following...	commit \| commitdiff \| tree
2008-04-09	Claudio Sacerdoti...	Added some "\n" here and there to the pretty-printing...	commit \| commitdiff \| tree
2008-04-09	Claudio Sacerdoti...	Grave bug fixed: Ce that point to definitions were...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Variables are no longer experted (cooking is now implemented).	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Swapped arguments in error message.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Variables having a body can occur in cooked terms and...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Fix over the previous one: Var-LetIn abstractions should...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Error message improved.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Cooking w.r.t. variables with bodies is now implemented...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Fix name capture in cofix.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	To test the translation.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Name capture fixed.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Improved error messages in place of "sort elimination...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Seed reset before each convert_obj.	commit \| commitdiff \| tree
next

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

RSS Atom