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

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

2005-07-12	Andrea Asperti	Added a function equations_for_goal similar to signature_of_...	commit \| commitdiff \| tree
2005-07-11	Andrea Asperti	aliases are now compared not only looking at the domain_item...	commit \| commitdiff \| tree
2005-07-11	Andrea Asperti	only regular files are ending in .ma are now searched	commit \| commitdiff \| tree
2005-07-11	Andrea Asperti	New version of the library, a bit more structured.	commit \| commitdiff \| tree
2005-07-11	Andrea Asperti	Removed the old library.	commit \| commitdiff \| tree
2005-07-07	Andrea Asperti	Check function for Matita name convention.	commit \| commitdiff \| tree
2005-07-07	Andrea Asperti	Raising an error on a bad theorem name.	commit \| commitdiff \| tree
2005-06-23	Andrea Asperti	Added Z, Zplus and its properties.	commit \| commitdiff \| tree
2005-06-16	Andrea Asperti	A cleaned version of auto_tac_new.	commit \| commitdiff \| tree
2005-06-09	Andrea Asperti	Updated to the new syntax for match.	commit \| commitdiff \| tree
2005-06-07	Andrea Asperti	My two pennies.	commit \| commitdiff \| tree
2005-05-31	Andrea Asperti	added colors	commit \| commitdiff \| tree
2005-05-31	Andrea Asperti	more verbose case failure message	commit \| commitdiff \| tree
2005-05-31	Andrea Asperti	added chronometer	commit \| commitdiff \| tree
2005-05-31	Andrea Asperti	added automathic aliases for _ind _rec and _rect when...	commit \| commitdiff \| tree
2005-05-31	Andrea Asperti	fix	commit \| commitdiff \| tree
2005-05-30	Andrea Asperti	fix	commit \| commitdiff \| tree
2005-05-30	Andrea Asperti	added intros n	commit \| commitdiff \| tree
2005-05-30	Andrea Asperti	added intros n.	commit \| commitdiff \| tree
2005-05-30	Andrea Asperti	added automathic aliases.	commit \| commitdiff \| tree
2005-05-27	Andrea Asperti	1. removed obsolete comments	commit \| commitdiff \| tree
2005-05-24	Andrea Asperti	fix	commit \| commitdiff \| tree
2005-05-24	Andrea Asperti	Added a new tactic elim_intros (without simpl of the...	commit \| commitdiff \| tree
2005-05-24	Andrea Asperti	elim -> elim_intros (no simpl)	commit \| commitdiff \| tree
2005-05-23	Andrea Asperti	Added andrea.ma	commit \| commitdiff \| tree
2005-05-20	Andrea Asperti	When we unify a Prod against a term t2 which is not...	commit \| commitdiff \| tree
2005-05-20	Andrea Asperti	Added a whd on ty in new_metasenv for apply, in order...	commit \| commitdiff \| tree
2005-05-20	Andrea Asperti	Hint repaired (an erroneous commit by myself).	commit \| commitdiff \| tree
2005-05-05	Andrea Asperti	test_instance.ma	commit \| commitdiff \| tree
2005-05-05	Andrea Asperti	Some modifications due to instance.	commit \| commitdiff \| tree
2005-05-03	Andrea Asperti	First version of instance.	commit \| commitdiff \| tree
2004-12-07	Andrea Asperti	symmetry of equality NOT used in auto	commit \| commitdiff \| tree
2004-12-06	Andrea Asperti	New version of auto with "width".	commit \| commitdiff \| tree
2004-11-30	Andrea Asperti	Bug in the management of substitutions into auto corrected.	commit \| commitdiff \| tree
2004-11-09	Andrea Asperti	Aggiunta l'introduzione alla prima sezione:.	commit \| commitdiff \| tree
2004-11-08	Andrea Asperti	First draft (introduction).	commit \| commitdiff \| tree
2004-11-04	Andrea Asperti	Auto moved to a new file autoTactic.ml	commit \| commitdiff \| tree
2004-11-04	Andrea Asperti	New version(s) of hint. One more stable (hint) and...	commit \| commitdiff \| tree
2004-11-04	Andrea Asperti	Added a new boolean parameter "facts" (default=false...	commit \| commitdiff \| tree
2004-11-04	Andrea Asperti	Porting to the new version of auto.	commit \| commitdiff \| tree
2004-10-27	Andrea Asperti	Bug fixing.	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	implemented elim query	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	bugfix: handle overflow in powerset cardinality	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- added (hack) apply_tac_verbose (for auto)	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	ported to typed explicit subst	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	be more quiet (removed debugging prints)	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	ported to typed explicit subst	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	rebuilt	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- ported to typed explicit subst	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- ported to typed explicit subst	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- ported to typed explicit substitutions	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- ported to typed explicit substitutions	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	cleanup temp files on parser failure	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	- reimplemented meta_closed in non CPS way (faster!)	commit \| commitdiff \| tree
2004-10-22	Andrea Asperti	added type to explicit substitutions	commit \| commitdiff \| tree
2004-10-20	Andrea Asperti	- removed cic_cache and cic_annotations_cache	commit \| commitdiff \| tree
2004-10-13	Andrea Asperti	get_and_save now handles big files properly (i.e. doesn...	commit \| commitdiff \| tree
2004-09-06	Andrea Asperti	Corrected bug about the generation of constraitns:...	commit \| commitdiff \| tree
2004-09-01	Andrea Asperti	Bug fixing: the call to MQueryMisc.wrong_xpointer_format_fro...	commit \| commitdiff \| tree
2004-07-20	Andrea Asperti	The type substitution has been moved into Cic.	commit \| commitdiff \| tree
2004-07-20	Andrea Asperti	Subst has been added to the kernel.	commit \| commitdiff \| tree
2004-07-01	Andrea Asperti	...	commit \| commitdiff \| tree
2004-06-28	Andrea Asperti	removed a useless test on explicit substitutions on...	commit \| commitdiff \| tree
2004-06-28	Andrea Asperti	use get_obj to retrieve cic objects instead of typecheck	commit \| commitdiff \| tree
2004-06-28	Andrea Asperti	fixed typo	commit \| commitdiff \| tree
2004-06-28	Andrea Asperti	- new implementation of the apply case in fo_unif using...	commit \| commitdiff \| tree
2004-06-16	Andrea Asperti	first moogle commit	commit \| commitdiff \| tree
2004-05-19	Andrea Asperti	first moogle template checkin	commit \| commitdiff \| tree
2004-05-18	Andrea Asperti	Nuova implementazione di Auto "breadth-first".	commit \| commitdiff \| tree
2004-05-10	Andrea Asperti	* empty log message *	commit \| commitdiff \| tree
2004-05-10	Andrea Asperti	Adding file newConstraint	commit \| commitdiff \| tree
2004-05-10	Andrea Asperti	Adding file match_concl	commit \| commitdiff \| tree
2004-04-15	Andrea Asperti	Metasenv added as parameter to eta_fixing.	commit \| commitdiff \| tree
2004-04-05	Andrea Asperti	Added a new function in_cache to cicEnvironemt. It...	commit \| commitdiff \| tree
2004-03-16	Andrea Asperti	Sorts are no longer all convertible. To be completed...	commit \| commitdiff \| tree
2004-03-16	Andrea Asperti	Sorts are no longer all convertible. To be completed...	commit \| commitdiff \| tree
2004-03-15	Andrea Asperti	This fails.	commit \| commitdiff \| tree
2004-02-19	Andrea Asperti	Adding tacticAst2Box (pretty printer for tactical,...	commit \| commitdiff \| tree
2004-02-19	Andrea Asperti	Minor modification in test_parser (to use the new pretty...	commit \| commitdiff \| tree
2004-02-13	Andrea Asperti	new (box based) pretty printer	commit \| commitdiff \| tree
2004-02-06	Andrea Asperti	Bug MutCase fixed: now the type of the constructor...	commit \| commitdiff \| tree
2004-02-04	Andrea Asperti	delift no longer apply the substitution when a Meta...	commit \| commitdiff \| tree
2004-02-04	Andrea Asperti	Added a new example.	commit \| commitdiff \| tree
2004-01-27	Andrea Asperti	test for empty string given, if so return Environment...	commit \| commitdiff \| tree
2004-01-26	Andrea Asperti	Notation for Case revisited and completed.	commit \| commitdiff \| tree
2004-01-22	Andrea Asperti	Now applying ocaml transformations to sequents as well.	commit \| commitdiff \| tree
2004-01-22	Andrea Asperti	A few modifications, here and there...	commit \| commitdiff \| tree
2004-01-22	Andrea Asperti	Added all transformations for sequents.	commit \| commitdiff \| tree
2004-01-20	Andrea Asperti	First version of refine for MutCase, still largely...	commit \| commitdiff \| tree
2003-10-01	Andrea Asperti	* the main function MUST return 0 to communicate everything...	commit \| commitdiff \| tree
2003-10-01	Andrea Asperti	* new version of metadata extraction	commit \| commitdiff \| tree
2003-07-30	Andrea Asperti	Eta fixing for MTCases added (that meant to recursively...	commit \| commitdiff \| tree
2003-07-29	Andrea Asperti	Added method FalseInd	commit \| commitdiff \| tree
2003-07-29	Andrea Asperti	Added method "FalseInd".	commit \| commitdiff \| tree
2003-07-29	Andrea Asperti	Added method AndInd.	commit \| commitdiff \| tree
2003-07-28	Andrea Asperti	Added Method "exists".	commit \| commitdiff \| tree
2003-07-28	Andrea Asperti	Few modif in eta-fixing.	commit \| commitdiff \| tree
2003-07-24	Andrea Asperti	Complete beta reduction added to avoid strange case...	commit \| commitdiff \| tree
2003-07-24	Andrea Asperti	Exact handled in a better way (no more "NO PROOFS").	commit \| commitdiff \| tree
2003-07-24	Andrea Asperti	The name of TD proofs was erroneously always set to...	commit \| commitdiff \| tree
next

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

RSS Atom