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

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

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
2009-05-21	Ferruccio Guidi	- cicUtil: is_sober now detects non-positive rels.	commit \| commitdiff \| tree \| snapshot
2009-05-21	Andrea Asperti	autobatch -> autobatch by	commit \| commitdiff \| tree \| snapshot
2009-05-20	Ferruccio Guidi	we catch the refiner errors in the critical step and...	commit \| commitdiff \| tree \| snapshot
2009-05-20	Andrea Asperti	Removed a silly type check	commit \| commitdiff \| tree \| snapshot
2009-05-19	Enrico Tassi	...	commit \| commitdiff \| tree \| snapshot
2009-05-19	Andrea Asperti	NotEq is now considered as a negative Eq atom	commit \| commitdiff \| tree \| snapshot
2009-05-19	Enrico Tassi	regenerated	commit \| commitdiff \| tree \| snapshot
2009-05-19	Enrico Tassi	fixed generation of horn clauses, negated atoms are...	commit \| commitdiff \| tree \| snapshot
2009-05-19	Enrico Tassi	some horn+equality problems	commit \| commitdiff \| tree \| snapshot
2009-05-18	Claudio Sacerdoti...	removed byte queries	commit \| commitdiff \| tree \| snapshot
2009-05-18	Enrico Tassi	removed useless function	commit \| commitdiff \| tree \| snapshot
2009-05-18	Enrico Tassi	in the new kernel you can type Type[i] to mean Type_i...	commit \| commitdiff \| tree \| snapshot
2009-05-18	Enrico Tassi	nothing special	commit \| commitdiff \| tree \| snapshot
2009-05-18	Claudio Sacerdoti...	1) GrafiteAst.NEval => GrafiteAst.NReduce	commit \| commitdiff \| tree \| snapshot
2009-05-18	Claudio Sacerdoti...	1) new tactic normalize (low-level function implemented in	commit \| commitdiff \| tree \| snapshot
2009-05-18	Claudio Sacerdoti...	1) order of processing of case branches reverted (to...	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	maxmeta implemented	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	maxmeta function to return the heighest meta used so far	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	alpha_eq exported	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	alpha_eq defined and exported	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	efficiency improvement (buffers are now used everywhere)	commit \| commitdiff \| tree \| snapshot
2009-05-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-17	Enrico Tassi	byte tests disabled	commit \| commitdiff \| tree \| snapshot
2009-05-15	Enrico Tassi	added patch to not unify any term containing the in_sco...	commit \| commitdiff \| tree \| snapshot
2009-05-15	Claudio Sacerdoti...	Patch to add a debugging string to HExtlib.split_nth...	commit \| commitdiff \| tree \| snapshot
2009-05-15	Claudio Sacerdoti...	Cosmetic.	commit \| commitdiff \| tree \| snapshot
2009-05-14	Ferruccio Guidi	- hExtlib: added debugging information for split_nth	commit \| commitdiff \| tree \| snapshot
2009-05-14	Ferruccio Guidi	- libraryObjects: new default "natural numbers" with...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Ferruccio Guidi	interpretations placed right after the corresponding...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Ferruccio Guidi	- matitaEngine: some commands like "coercion" must...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	The singature of the "by" universe is added to the...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Via un'altra linea...	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Sempre piu' breve	commit \| commitdiff \| tree \| snapshot
2009-05-13	Andrea Asperti	Signature is computed on the initial goal, once and...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Claudio Sacerdoti...	Do we really want to generate eliminators for nested...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Claudio Sacerdoti...	All weakly positive types but imbricated ones are now...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Ferruccio Guidi	- Procedural: we now reconstruct "let H := v in t"...	commit \| commitdiff \| tree \| snapshot
2009-05-12	Andrea Asperti	We only filter the smart candidates w.r.t the signature	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Some experiments in generation of elimination principles.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	ppsubst commented out in ppobj	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Bug fixed: the relevance list can be shorted then leftn...	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Missing spaces inserted here and there.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	- non_punctuational_tacticals ported to NG	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	Buffers are now used everywhere for speed-up.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Claudio Sacerdoti...	New function list_iter_sep.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Andrea Asperti	A few lemmas about inclusion.	commit \| commitdiff \| tree \| snapshot
2009-05-11	Andrea Asperti	More automation	commit \| commitdiff \| tree \| snapshot
2009-05-10	Claudio Sacerdoti...	- critical bug fixed in NCicSubstitution.lift:	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Stupid typing error fixed.	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed: left parameters of constructors were unified...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed: refinement of mutual recursive definitions...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Improved tests (for left parameters and mutual recursiv...	commit \| commitdiff \| tree \| snapshot
2009-05-08	Claudio Sacerdoti...	Bug fixed in refinement of inductive types: left parame...	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom