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

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

2009-06-18	denes	Fixed wrong types in proof terms	commit \| commitdiff \| tree \| snapshot
2009-06-18	Claudio Sacerdoti...	Stricter type: the type now shows that disambiguation...	commit \| commitdiff \| tree \| snapshot
2009-06-18	Claudio Sacerdoti...	1) grafiteWalker removed	commit \| commitdiff \| tree \| snapshot
2009-06-17	Enrico Tassi	proof reconstruction almost OK	commit \| commitdiff \| tree \| snapshot
2009-06-17	Claudio Sacerdoti...	Initial implementation of statuses using objects in...	commit \| commitdiff \| tree \| snapshot
2009-06-17	denes	Added optionnal one pass simplification (instead of...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	first proof reconstruction attempt, still bugged since it	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	1) unification hint now takes NG terms (as it should...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	1) NCicLibrary (which is untrusted) moved after NCicUnt...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	Implementation of existential type improved (more stric...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	avoid fixing non-recursive terms	commit \| commitdiff \| tree \| snapshot
2009-06-16	Enrico Tassi	we fix recursive object reference with the correct...	commit \| commitdiff \| tree \| snapshot
2009-06-16	Claudio Sacerdoti...	FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:	commit \| commitdiff \| tree \| snapshot
2009-06-16	Ferruccio Guidi	we corrected some reduction bugs about renaming.	commit \| commitdiff \| tree \| snapshot
2009-06-15	Ferruccio Guidi	we removed some old code and fixed a reduction bug...	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (part B, by CSC :-):	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (by CSC,actuall :-)	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	added TODO list	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	huge commit regarding the grafite_status:	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	part of last commit	commit \| commitdiff \| tree \| snapshot
2009-06-15	Enrico Tassi	tacticals are really tactics now, they have an AST...	commit \| commitdiff \| tree \| snapshot
2009-06-13	Ferruccio Guidi	we removed some coercion detours and we added some...	commit \| commitdiff \| tree \| snapshot
2009-06-12	denes	Implemented keep_simplified.	commit \| commitdiff \| tree \| snapshot
2009-06-12	Claudio Sacerdoti...	ocaml sucks...	commit \| commitdiff \| tree \| snapshot
2009-06-12	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-06-12	Enrico Tassi	-ng implemented	commit \| commitdiff \| tree \| snapshot
2009-06-12	Andrea Asperti	Added a new keep_simplified function	commit \| commitdiff \| tree \| snapshot
2009-06-12	Andrea Asperti	Renamed forward_simplify into simplify and backward_sim...	commit \| commitdiff \| tree \| snapshot
2009-06-11	denes	Active goals are now demodulated after selecting a...	commit \| commitdiff \| tree \| snapshot
2009-06-11	Ferruccio Guidi	- applyTransformation: bugfix in the rendering of records	commit \| commitdiff \| tree \| snapshot
2009-06-11	Enrico Tassi	content2pres for the new cic fixed	commit \| commitdiff \| tree \| snapshot
2009-06-11	Ferruccio Guidi	- some depend files fixed	commit \| commitdiff \| tree \| snapshot
2009-06-10	Ferruccio Guidi	- library/list/list.ma: unused code commented	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	1) added simplification of actives w.r.t. selected	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	right inference step completed	commit \| commitdiff \| tree \| snapshot
2009-06-10	Enrico Tassi	new function filter_map_acc	commit \| commitdiff \| tree \| snapshot
2009-06-10	denes	Extended the equality case to non ground terms	commit \| commitdiff \| tree \| snapshot
2009-06-09	Ferruccio Guidi	- Procedural: more support for the Debug inline option...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Claudio Sacerdoti...	Debugging code removed.	commit \| commitdiff \| tree \| snapshot
2009-06-09	Claudio Sacerdoti...	Temporary (and partially broken) patch for Ferruccio...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	almost complete superposition right step	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	snapshot	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	see the previous commit	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	termAcicContent is logic independent (despite its name...	commit \| commitdiff \| tree \| snapshot
2009-06-09	denes	Optimized weigths comparison, removed normalization	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	snaphost: supright almost done	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	denes	Implemented substitution application and concatenation	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	fixed metas	commit \| commitdiff \| tree \| snapshot
2009-06-09	Enrico Tassi	fixed building	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	a skeleton of supright	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	some more functors and a nice higher-order all_position...	commit \| commitdiff \| tree \| snapshot
2009-06-08	Enrico Tassi	added META for ng_paramodulation	commit \| commitdiff \| tree \| snapshot
2009-06-06	Claudio Sacerdoti...	Previous commit reverted, as explained in that log.	commit \| commitdiff \| tree \| snapshot
2009-06-06	Claudio Sacerdoti...	This commit restores the ids_to_father_ids table.	commit \| commitdiff \| tree \| snapshot
2009-06-06	Enrico Tassi	some renaming to make ocamlopt happy	commit \| commitdiff \| tree \| snapshot
2009-06-05	Ferruccio Guidi	bugfix in Include syntax: it was changed and committed...	commit \| commitdiff \| tree \| snapshot
2009-06-05	Ferruccio Guidi	- Procedural convertible rewrites in the conclusion...	commit \| commitdiff \| tree \| snapshot
2009-06-05	denes	First tests for paramodulation (pretty printer, unifica...	commit \| commitdiff \| tree \| snapshot
2009-06-05	Wilmer Ricciotti	- replaced part1a/defn with the version based on induct...	commit \| commitdiff \| tree \| snapshot
2009-06-05	denes	Fix : wrong exception was catch in apply_subst	commit \| commitdiff \| tree \| snapshot
2009-06-05	Claudio Sacerdoti...	1) the home button of CicBrowser now works also for NG	commit \| commitdiff \| tree \| snapshot
2009-06-05	Claudio Sacerdoti...	The kernel _must_ check the correctness of the height...	commit \| commitdiff \| tree \| snapshot
2009-06-04	Ferruccio Guidi	syntax error fixed :(	commit \| commitdiff \| tree \| snapshot
2009-06-04	Ferruccio Guidi	- doubleTypeInference: we check for unreferenced letins...	commit \| commitdiff \| tree \| snapshot
2009-06-04	denes	First pretty printing functions	commit \| commitdiff \| tree \| snapshot
2009-06-04	Enrico Tassi	minor changes here and there. We extend fo-unification...	commit \| commitdiff \| tree \| snapshot
2009-06-04	Enrico Tassi	comments	commit \| commitdiff \| tree \| snapshot
2009-06-04	Enrico Tassi	better type for comparison and implementation of KBO...	commit \| commitdiff \| tree \| snapshot
2009-06-04	Enrico Tassi	more functors	commit \| commitdiff \| tree \| snapshot
2009-06-03	Ferruccio Guidi	- boxPp: added missing spaces	commit \| commitdiff \| tree \| snapshot
2009-06-03	Wilmer Ricciotti	Update, using induction/inversion.	commit \| commitdiff \| tree \| snapshot
2009-06-03	Enrico Tassi	functorial abstraction over term blobs	commit \| commitdiff \| tree \| snapshot
2009-06-03	Andrea Asperti	not_to_not	commit \| commitdiff \| tree \| snapshot
2009-06-03	Claudio Sacerdoti...	New test for NG notation.	commit \| commitdiff \| tree \| snapshot
2009-06-03	Claudio Sacerdoti...	Huge commit with several changes:	commit \| commitdiff \| tree \| snapshot
2009-06-01	denes	First implementation of unification on foterms	commit \| commitdiff \| tree \| snapshot
2009-06-01	denes	First functions on substitutions for unification	commit \| commitdiff \| tree \| snapshot
2009-06-01	Enrico Tassi	added a snapshot of comparison	commit \| commitdiff \| tree \| snapshot
2009-06-01	Andrea Asperti	This works for me	commit \| commitdiff \| tree \| snapshot
2009-06-01	Enrico Tassi	we rewrite the paramodulation code!	commit \| commitdiff \| tree \| snapshot
2009-05-29	Wilmer Ricciotti	POPLmark part 1a using the de Bruijn encoding.	commit \| commitdiff \| tree \| snapshot
2009-05-29	Ferruccio Guidi	- cicNotationParser: added extra space to TeX control...	commit \| commitdiff \| tree \| snapshot
2009-05-28	Ferruccio Guidi	Procedural: higher-order unification needs a lot of...	commit \| commitdiff \| tree \| snapshot
2009-05-28	Ferruccio Guidi	- cicInspect: relevant nodes count updated: letin nodes...	commit \| commitdiff \| tree \| snapshot
2009-05-27	Ferruccio Guidi	Procedural: bugfix in the generation of intros for...	commit \| commitdiff \| tree \| snapshot
2009-05-27	Ferruccio Guidi	- Procedural: we specify more unifiers for apply to...	commit \| commitdiff \| tree \| snapshot
2009-05-27	Claudio Sacerdoti...	Basic support for interpretations for NG:	commit \| commitdiff \| tree \| snapshot
2009-05-27	Andrea Asperti	Avoiding to filter the application of congruence equations	commit \| commitdiff \| tree \| snapshot
2009-05-26	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-26	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-26	Andrea Asperti	removed a call to autobatch.	commit \| commitdiff \| tree \| snapshot
2009-05-25	Enrico Tassi	nasty change in the lexer/parser:	commit \| commitdiff \| tree \| snapshot
2009-05-22	Ferruccio Guidi	bugfix in the output notation for eq	commit \| commitdiff \| tree \| snapshot
2009-05-22	Andrea Asperti	Pruning candidates in the applicative case for equalities.	commit \| commitdiff \| tree \| snapshot
2009-05-21	Ferruccio Guidi	Procedural: we use the expected type rather than the...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom