matita.cs.unibo.it Git - helm.git/history - helm/software/components/grafite

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/grafite_engine/grafiteEngine.ml

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	blob \| commitdiff \| raw
2010-02-08	Andrea Asperti	Bug fixing.	blob \| commitdiff \| raw \| diff to current
2010-02-03	Claudio Sacerdoti...	Parts of the status were not re-initialized correctly...	blob \| commitdiff \| raw \| diff to current
2010-01-08	Andrea Asperti	refresh uri	blob \| commitdiff \| raw \| diff to current
2009-12-09	Andrea Asperti	Added the paramodulation active/passive tables to the...	blob \| commitdiff \| raw \| diff to current
2009-11-16	Wilmer Ricciotti	Implementation of ndestruct tactic (including destructi...	blob \| commitdiff \| raw \| diff to current
2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	blob \| commitdiff \| raw \| diff to current
2009-10-21	Enrico Tassi	add XXX where I found a catch all statement	blob \| commitdiff \| raw \| diff to current
2009-10-16	Enrico Tassi	better indexing for auto	blob \| commitdiff \| raw \| diff to current
2009-10-12	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2009-10-07	Enrico Tassi	terms indexed in the automation cache are saturated	blob \| commitdiff \| raw \| diff to current
2009-10-07	Enrico Tassi	fixed Ref generation	blob \| commitdiff \| raw \| diff to current
2009-10-06	Wilmer Ricciotti	Inverters/Inversion:	blob \| commitdiff \| raw \| diff to current
2009-10-06	Enrico Tassi	nAuto W.I.P.	blob \| commitdiff \| raw \| diff to current
2009-10-05	Enrico Tassi	auto and auto_paramod are in nAuto	blob \| commitdiff \| raw \| diff to current
2009-10-05	Enrico Tassi	added auto_cache in the dupable status after an	blob \| commitdiff \| raw \| diff to current
2009-10-05	Enrico Tassi	new ng_library module	blob \| commitdiff \| raw \| diff to current
2009-10-02	Enrico Tassi	fixed bug in coercion application, input/output swapped...	blob \| commitdiff \| raw \| diff to current
2009-10-02	Wilmer Ricciotti	Updated command ninverter. Syntax:	blob \| commitdiff \| raw \| diff to current
2009-09-30	Wilmer Ricciotti	Added initial support for inversion principles in Matit...	blob \| commitdiff \| raw \| diff to current
2009-09-21	Enrico Tassi	huge commit regarding universes:	blob \| commitdiff \| raw \| diff to current
2009-09-14	Enrico Tassi	fixed coercion mechanism w.r.t. undo/require	blob \| commitdiff \| raw \| diff to current
2009-09-14	Claudio Sacerdoti...	New tactics ncut and nlapply.	blob \| commitdiff \| raw \| diff to current
2009-09-11	Enrico Tassi	constructor accepts the arguments of the constructor...	blob \| commitdiff \| raw \| diff to current
2009-09-11	Enrico Tassi	new tactic constructor: @[n]	blob \| commitdiff \| raw \| diff to current
2009-09-11	Enrico Tassi	new macro ncheck. fixed term2pres for Inductive and...	blob \| commitdiff \| raw \| diff to current
2009-09-09	Enrico Tassi	some more work for ng-coercions	blob \| commitdiff \| raw \| diff to current
2009-09-08	Enrico Tassi	snapshot for CSC	blob \| commitdiff \| raw \| diff to current
2009-07-31	Claudio Sacerdoti...	Serious bug fixed: uris were not refreshed when loading...	blob \| commitdiff \| raw \| diff to current
2009-07-24	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw \| diff to current
2009-07-24	Claudio Sacerdoti...	Record fields declared as coercions as now really decla...	blob \| commitdiff \| raw \| diff to current
2009-07-22	Claudio Sacerdoti...	Almost ready to implement coercion declaration for...	blob \| commitdiff \| raw \| diff to current
2009-07-21	Claudio Sacerdoti...	Record projections are now automatically generated...	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	1) the user is notified when a new object is defined	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	Generation of principles is now atomic.	blob \| commitdiff \| raw \| diff to current
2009-07-17	Enrico Tassi	add comment	blob \| commitdiff \| raw \| diff to current
2009-07-17	Claudio Sacerdoti...	Generation of inductive principle for Type[0].	blob \| commitdiff \| raw \| diff to current
2009-07-15	Enrico Tassi	ncopy partially implemented and fixed (a ?) chain to...	blob \| commitdiff \| raw \| diff to current
2009-07-14	denes	Fixed Option type error (OCaml bug)	blob \| commitdiff \| raw \| diff to current
2009-07-10	Enrico Tassi	initial implementation of coercion composition	blob \| commitdiff \| raw \| diff to current
2009-07-10	Claudio Sacerdoti...	Bug fixed (missing ctx) + comment added.	blob \| commitdiff \| raw \| diff to current
2009-07-09	Enrico Tassi	initial implementation of `ncoercion name : type :...	blob \| commitdiff \| raw \| diff to current
2009-07-09	Enrico Tassi	new nrepeat (and block '('...')' ) tactical	blob \| commitdiff \| raw \| diff to current
2009-07-08	Claudio Sacerdoti...	Bug fixed: the debrujinate function (hence the one...	blob \| commitdiff \| raw \| diff to current
2009-07-07	Claudio Sacerdoti...	1) Include files for NG were neither recursively proces...	blob \| commitdiff \| raw \| diff to current
2009-06-23	Enrico Tassi	undo/serialization for universes implemented	blob \| commitdiff \| raw \| diff to current
2009-06-23	Claudio Sacerdoti...	1) NCicTypechecker.typecheck_obj removed, since it...	blob \| commitdiff \| raw \| diff to current
2009-06-19	Claudio Sacerdoti...	Estatus finally merged into the global status using...	blob \| commitdiff \| raw \| diff to current
2009-06-19	Claudio Sacerdoti...	Useless GrafiteTypes.get_baseuri removed.	blob \| commitdiff \| raw \| diff to current
2009-06-19	Claudio Sacerdoti...	More statuses converted to objects.	blob \| commitdiff \| raw \| diff to current
2009-06-18	Enrico Tassi	debug pps removed	blob \| commitdiff \| raw \| diff to current
2009-06-18	Claudio Sacerdoti...	Objects are now used to represent also the tactic status.	blob \| commitdiff \| raw \| diff to current
2009-06-18	denes	Added ntry and nassumption tactics	blob \| commitdiff \| raw \| diff to current
2009-06-18	Claudio Sacerdoti...	1) grafiteWalker removed	blob \| commitdiff \| raw \| diff to current
2009-06-17	Claudio Sacerdoti...	Initial implementation of statuses using objects in...	blob \| commitdiff \| raw \| diff to current
2009-06-16	Claudio Sacerdoti...	1) unification hint now takes NG terms (as it should...	blob \| commitdiff \| raw \| diff to current
2009-06-16	Enrico Tassi	avoid fixing non-recursive terms	blob \| commitdiff \| raw \| diff to current
2009-06-16	Enrico Tassi	we fix recursive object reference with the correct...	blob \| commitdiff \| raw \| diff to current
2009-06-16	Claudio Sacerdoti...	FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:	blob \| commitdiff \| raw \| diff to current
2009-06-15	Enrico Tassi	EXPERIMENTAL COMMIT (by CSC,actuall :-)	blob \| commitdiff \| raw \| diff to current
2009-06-15	Enrico Tassi	huge commit regarding the grafite_status:	blob \| commitdiff \| raw \| diff to current
2009-06-15	Enrico Tassi	part of last commit	blob \| commitdiff \| raw \| diff to current
2009-06-09	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2009-06-05	denes	First tests for paramodulation (pretty printer, unifica...	blob \| commitdiff \| raw \| diff to current
2009-06-05	Claudio Sacerdoti...	The kernel _must_ check the correctness of the height...	blob \| commitdiff \| raw \| diff to current
2009-06-03	Claudio Sacerdoti...	Huge commit with several changes:	blob \| commitdiff \| raw \| diff to current
2009-05-28	Ferruccio Guidi	- cicInspect: relevant nodes count updated: letin nodes...	blob \| commitdiff \| raw \| diff to current
2009-05-25	Enrico Tassi	nasty change in the lexer/parser:	blob \| commitdiff \| raw \| diff to current
2009-05-18	Enrico Tassi	in the new kernel you can type Type[i] to mean Type_i...	blob \| commitdiff \| raw \| diff to current
2009-05-18	Claudio Sacerdoti...	1) GrafiteAst.NEval => GrafiteAst.NReduce	blob \| commitdiff \| raw \| diff to current
2009-05-11	Claudio Sacerdoti...	- non_punctuational_tacticals ported to NG	blob \| commitdiff \| raw \| diff to current
2009-05-08	Claudio Sacerdoti...	1) better implementation of NObj that now calls recursi...	blob \| commitdiff \| raw \| diff to current
2009-05-05	Enrico Tassi	- pretty printer made robust in face of list_nth	blob \| commitdiff \| raw \| diff to current
2009-04-28	Enrico Tassi	huge commit in automation:	blob \| commitdiff \| raw \| diff to current
2009-04-26	Claudio Sacerdoti...	The backward compatible management of aliases for NG...	blob \| commitdiff \| raw \| diff to current
2009-04-25	Claudio Sacerdoti...	It is now possible for commands processed by grafiteEng...	blob \| commitdiff \| raw \| diff to current
2009-04-24	Claudio Sacerdoti...	- Grammar for all obj commands ported to NG (let recs...	blob \| commitdiff \| raw \| diff to current
2009-04-24	Claudio Sacerdoti...	Quick&dirty implementation of neqd:	blob \| commitdiff \| raw \| diff to current
2009-04-22	Wilmer Ricciotti	New command "inverter" used to generate an induction...	blob \| commitdiff \| raw \| diff to current
2009-04-20	Enrico Tassi	- init_cache_and_tables rewritten using the automation_...	blob \| commitdiff \| raw \| diff to current
2009-04-16	Enrico Tassi	Universe is used only locally to tactics/	blob \| commitdiff \| raw \| diff to current
2009-04-14	Claudio Sacerdoti...	assert_tac now takes a list of sequents and also checks...	blob \| commitdiff \| raw \| diff to current
2009-04-14	Claudio Sacerdoti...	New debugging tactic nassert:	blob \| commitdiff \| raw \| diff to current
2009-04-09	Enrico Tassi	added letin, still broken	blob \| commitdiff \| raw \| diff to current
2009-04-09	Enrico Tassi	new tactic whd implemented	blob \| commitdiff \| raw \| diff to current
2009-04-08	Enrico Tassi	generalized is half-implemented (still broken)	blob \| commitdiff \| raw \| diff to current
2009-04-07	Claudio Sacerdoti...	- nrewrite ((very?) rough implementation)	blob \| commitdiff \| raw \| diff to current
2009-04-06	Enrico Tassi	tactic cases works! delift clears tags	blob \| commitdiff \| raw \| diff to current
2009-04-02	Enrico Tassi	...	blob \| commitdiff \| raw \| diff to current
2009-04-01	Claudio Sacerdoti...	New tactic "case1_tac" that make "intro" followed by...	blob \| commitdiff \| raw \| diff to current
2009-04-01	Claudio Sacerdoti...	New tactic intro. Syntax: "# n".	blob \| commitdiff \| raw \| diff to current
2009-04-01	Enrico Tassi	added tentative elim	blob \| commitdiff \| raw \| diff to current
2009-04-01	Enrico Tassi	1) mk_meta now returns also the index of the created...	blob \| commitdiff \| raw \| diff to current
2009-03-30	Enrico Tassi	tentative subst-sexpand and change	blob \| commitdiff \| raw \| diff to current
2009-03-26	Enrico Tassi	new apply almost there	blob \| commitdiff \| raw \| diff to current
2009-03-25	Enrico Tassi	new tactics are almost ready	blob \| commitdiff \| raw \| diff to current
2009-03-10	Enrico Tassi	unification hints almost ready	blob \| commitdiff \| raw \| diff to current
2009-01-13	Enrico Tassi	many changes regarding coercions:	blob \| commitdiff \| raw \| diff to current
2008-12-19	Enrico Tassi	added 'unification hint command to add a term to the...	blob \| commitdiff \| raw \| diff to current
2008-11-28	Ferruccio Guidi	ng_disambiguation ng_kernel ng_refiner disambiguation...	blob \| commitdiff \| raw \| diff to current
next

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

RSS Atom