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

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

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???) ...stylesheets to old plain ocaml code by Andrea Asperti.	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
2001-08-29	Andrea Asperti	1. Fixati alcuni problemi di indentazione con le rewrite.	commit \| commitdiff \| tree
2001-08-28	Andrea Asperti	Espansione dinamica delle prove per Mozilla/Galeon.	commit \| commitdiff \| tree
2001-07-26	Andrea Asperti	Bug in zarith notation corrected.	commit \| commitdiff \| tree
2001-07-25	Andrea Asperti	"Recursive" notation for Z.	commit \| commitdiff \| tree
2001-07-05	Andrea Asperti	Notation for ZArith (inside arith.xsl) added.	commit \| commitdiff \| tree
2001-06-29	Andrea Asperti	":" bug in theory_pres fixed.	commit \| commitdiff \| tree
2001-06-29	Andrea Asperti	small error inside mk_meta_theory.	commit \| commitdiff \| tree
2001-06-29	Andrea Asperti	mk_meta_theory.xsl added	commit \| commitdiff \| tree
2001-06-29	Andrea Asperti	occurrences.xsl added	commit \| commitdiff \| tree
2001-06-18	Andrea Asperti	BUG LAMBDA fixed.	commit \| commitdiff \| tree
2001-06-18	Andrea Asperti	drop_coercions.xsl has been added	commit \| commitdiff \| tree
2001-05-15	Andrea Asperti	Aggiunto lambda.xsl	commit \| commitdiff \| tree
2001-05-15	Andrea Asperti	Lambda notazione.	commit \| commitdiff \| tree
2001-04-11	Andrea Asperti	In natural language, non vengono piu' stampati glia...	commit \| commitdiff \| tree
2001-04-05	Andrea Asperti	Bug nat_double_ind solved.	commit \| commitdiff \| tree
2001-04-03	Andrea Asperti	* empty log message *	commit \| commitdiff \| tree
2001-04-03	Andrea Asperti	Complete management of inductive types.	commit \| commitdiff \| tree
2001-03-07	Andrea Asperti	* empty log message *	commit \| commitdiff \| tree
2001-03-05	Andrea Asperti	added eq_ind	commit \| commitdiff \| tree
2001-02-20	Andrea Asperti	New stylesheets from content to html.	commit \| commitdiff \| tree
2001-02-07	Andrea Asperti	New version of proof.xsl	commit \| commitdiff \| tree
2001-01-25	Andrea Asperti	ex_ind treated similarly to exT_ind.	commit \| commitdiff \| tree
2001-01-25	Andrea Asperti	ExT_ind implemented.	commit \| commitdiff \| tree
2001-01-23	Andrea Asperti	- Bug due to overloading of csymbol letin fixed.	commit \| commitdiff \| tree

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

RSS Atom