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

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

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
2008-04-08	Claudio Sacerdoti...	Use seed to avoid further name clashes.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Incredible, but true! Our name mangling clashed with...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Cooked objects are no longer well typed in the uncooked...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Improved eat_prods error message (at the cost of passing...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	The old kernel does not accept ens whose order is different...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Bad alpha-conversion by Enrico fixed.	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	Bug fixed: the ens need not be ordered w.r.t. the declared...	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	j off by one in error message	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	fix_outty partially fixed: missing lifts in args and ens	commit \| commitdiff \| tree
2008-04-08	Claudio Sacerdoti...	fix_outty fixed in order to perform eta-expansion when...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Tentative (and bad!) fix of outtypes in non-dependent...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Cooking discriminated into cooking in types (using...	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Pretty-printing of definitions fixed.	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Cooking implemented (not tested yet).	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Reports improved.	commit \| commitdiff \| tree
2008-04-07	Claudio Sacerdoti...	Debugging code fixed.	commit \| commitdiff \| tree
2008-04-01	Claudio Sacerdoti...	typeof_obj0 implemented	commit \| commitdiff \| tree
2008-04-01	Claudio Sacerdoti...	1) added get_checked_indtys that returns the whole...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	Automatic generation of elimination and inversion principles...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	Large amount of duplicated code (still in comments...	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	1) Impredicative sort "Set" removed everywhere.	commit \| commitdiff \| tree
2008-03-31	Claudio Sacerdoti...	1) more sharing everywhere in NCicSubstitution	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	New syntax for auto-related tactics and conclude/obtain.	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	Script fixed (it did not compile due to a mistake before...	commit \| commitdiff \| tree
2008-03-20	Claudio Sacerdoti...	End of patch for computation of LetIn types. Now types...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Bug: types and terms pushed into the context must be...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	-debug improved	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	prerr_endline => debug_print	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Number notation for Coq is back again, waiting for...	commit \| commitdiff \| tree
2008-03-19	Claudio Sacerdoti...	Files committed by Enrico (a mistake, I suppose) removed.	commit \| commitdiff \| tree
2008-03-14	Claudio Sacerdoti...	Tests enabled again.	commit \| commitdiff \| tree
2008-03-13	Claudio Sacerdoti...	:-(	commit \| commitdiff \| tree
2008-03-13	Claudio Sacerdoti...	New version of freescale:	commit \| commitdiff \| tree
2008-03-12	Claudio Sacerdoti...	Problem solved (was: apply needed an argument to avoid...	commit \| commitdiff \| tree
2008-03-12	Claudio Sacerdoti...	Almost always correct optimization: during unification...	commit \| commitdiff \| tree
2008-03-11	Claudio Sacerdoti...	Very experimental commit: the type of the source is...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Bad hack to avoid failure of conversion (unfolding...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Scripts fixed because of:	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Tactic reduce got rid of. Use normalize, instead.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	whd: ~delta=false now controls also zeta-reduction...	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	An unimplemented case of clearbody is now implemented.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	check_metasenv_consistency:	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Example query fixed.	commit \| commitdiff \| tree
2008-03-10	Claudio Sacerdoti...	Debugging print removed.	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Added ad-hoc optimization for check_metasenv_consistency...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Performance improvement: let-ins should always be pushed...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Scripts fixed. They were broken since the change to...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Potentially (and, at least sometimes, actually) big...	commit \| commitdiff \| tree
2008-03-09	Claudio Sacerdoti...	Redundant check (because of an invariant) removed.	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	New syntax for patterns.	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	prodT ==> prod	commit \| commitdiff \| tree
2008-03-04	Claudio Sacerdoti...	A) New version.	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	A new very simple example for recursive functions....	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Avoid translating back recursive fixes to the same...	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Avoid application to 0 arguments.	commit \| commitdiff \| tree
2008-02-21	Claudio Sacerdoti...	Better handling of exceptions.	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	A formalization of modified realisability with truth...	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	Bug fixed in generation of elimination principles of...	commit \| commitdiff \| tree
2008-02-08	Claudio Sacerdoti...	prodT merged with prod	commit \| commitdiff \| tree
2008-02-07	Claudio Sacerdoti...	ProdT was a perfect copy of Prod. Removed.	commit \| commitdiff \| tree
next

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

RSS Atom