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

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

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
2003-07-24	Andrea Asperti	Improved management of conclusions, to avoid repetitions.	commit \| commitdiff \| tree
2003-07-23	Andrea Asperti	- better handling of proof expansion/contraction	commit \| commitdiff \| tree
2003-07-23	Andrea Asperti	- Lemma added to the list of proof arguments	commit \| commitdiff \| tree
2003-07-22	Andrea Asperti	Debugging stuff changed.	commit \| commitdiff \| tree
2003-07-22	Andrea Asperti	"Final" commit that patches termViewer while still...	commit \| commitdiff \| tree
2003-07-22	Andrea Asperti	Previous commit was erroneous and dit not compile.	commit \| commitdiff \| tree
2003-07-22	Andrea Asperti	1. Modificiations due to the change ot K.Aux	commit \| commitdiff \| tree
2003-07-21	Andrea Asperti	The Aux argument of conclude is now of type string...	commit \| commitdiff \| tree
2003-07-21	Andrea Asperti	UNTESTED	commit \| commitdiff \| tree
2003-07-21	Andrea Asperti	We do not compute inner-types for the metasenv ==>...	commit \| commitdiff \| tree
2003-07-21	Andrea Asperti	Rendering of current proofs completed.	commit \| commitdiff \| tree
2003-07-18	Andrea Asperti	CSC: tentative definition of the ocaml structure that...	commit \| commitdiff \| tree
2003-07-16	Andrea Asperti	Several changes (the beginning of a new era???)	commit \| commitdiff \| tree
2003-06-25	Andrea Asperti	It should have already been moved to ocaml/mathql_generator	commit \| commitdiff \| tree
2002-11-20	Andrea Asperti	Minor bug fixes:	commit \| commitdiff \| tree
2002-11-19	Andrea Asperti	New metadata for sort and rel.	commit \| commitdiff \| tree
2002-04-16	Andrea Asperti	1. CicReduction moved into CicReductionNaif	commit \| commitdiff \| tree
2002-04-16	Andrea Asperti	Replaced with a symbolic link to the actual implementation.	commit \| commitdiff \| tree
2002-04-16	Andrea Asperti	type_of_aux' exported.	commit \| commitdiff \| tree
2002-04-16	Andrea Asperti	Meta implemented.	commit \| commitdiff \| tree
2001-11-16	Andrea Asperti	Disequalities chains for algebra. First draft.	commit \| commitdiff \| tree
2001-11-05	Andrea Asperti	Algebra notation.	commit \| commitdiff \| tree
next

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

RSS Atom