matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/primitiveTactics.ml

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

[helm.git] / helm / software / components / tactics / primitiveTactics.ml

2009-02-03	Enrico Tassi	case tactic first tries with a simple outtype and then...	blob \| commitdiff \| raw
2008-09-26	Enrico Tassi	lazy proof term to increase sharing and decrease memory...	blob \| commitdiff \| raw \| diff to current
2008-07-02	Ferruccio Guidi	- new tactic applyP for use in the Procedural script...	blob \| commitdiff \| raw \| diff to current
2008-06-19	Claudio Sacerdoti...	1. bug fixed in generalize_pattern: a lazy const_tac...	blob \| commitdiff \| raw \| diff to current
2008-06-08	Claudio Sacerdoti...	Bug fixed: wrong default pattern for generalize.	blob \| commitdiff \| raw \| diff to current
2008-06-08	Claudio Sacerdoti...	Hypotheses patterns for elim implemented. No more need...	blob \| commitdiff \| raw \| diff to current
2008-05-30	Enrico Tassi	CProp hierarchy is there!	blob \| commitdiff \| raw \| diff to current
2008-04-22	Enrico Tassi	oblivion ugraph everywhere outside the kernel	blob \| commitdiff \| raw \| diff to current
2008-03-11	Claudio Sacerdoti...	Very experimental commit: the type of the source is...	blob \| commitdiff \| raw \| diff to current
2008-03-09	Claudio Sacerdoti...	Performance improvement: let-ins should always be pushe...	blob \| commitdiff \| raw \| diff to current
2007-07-18	Ferruccio Guidi	the predicate for elim was not built correctly when...	blob \| commitdiff \| raw \| diff to current
2007-06-13	Enrico Tassi	cut is now implemented building a letin and not a beta...	blob \| commitdiff \| raw \| diff to current
2007-05-18	Ferruccio Guidi	- new devel contribs/LAMBDA-TYPES/Base-2 with the autom...	blob \| commitdiff \| raw \| diff to current
2007-05-17	Enrico Tassi	added a (for the moment) dummy field _subst to Proofeng...	blob \| commitdiff \| raw \| diff to current
2007-05-09	Ferruccio Guidi	PrimitiveTactics: intros _ now aveilable	blob \| commitdiff \| raw \| diff to current
2007-05-03	Ferruccio Guidi	elim with a pattern now works correctly (hopefully)	blob \| commitdiff \| raw \| diff to current
2007-04-27	Andrea Asperti	Apply_with_subst now returns a subst with a correct...	blob \| commitdiff \| raw \| diff to current
2007-04-16	Enrico Tassi	simplify has a brand new semantics!	blob \| commitdiff \| raw \| diff to current
2007-04-10	Enrico Tassi	fixed case	blob \| commitdiff \| raw \| diff to current
2007-04-10	Enrico Tassi	you can case even if only a right appears... so, substi...	blob \| commitdiff \| raw \| diff to current
2007-04-04	Ferruccio Guidi	alpha equivalence test factorized and moved to CicUtil	blob \| commitdiff \| raw \| diff to current
2007-04-03	Enrico Tassi	new case implementation	blob \| commitdiff \| raw \| diff to current
2007-04-02	Enrico Tassi	hopefully fixed cases implementation	blob \| commitdiff \| raw \| diff to current
2007-03-16	Ferruccio Guidi	elim tactic: it needs two arguments, a term as well...	blob \| commitdiff \| raw \| diff to current
2007-03-13	Ferruccio Guidi	elim tactic: now takes a pattern instead of just a...	blob \| commitdiff \| raw \| diff to current
2007-02-27	Ferruccio Guidi	- Procedural: some improvements	blob \| commitdiff \| raw \| diff to current
2007-02-14	Ferruccio Guidi	Procedural : some improvements	blob \| commitdiff \| raw \| diff to current
2007-02-09	Claudio Sacerdoti...	Debugging code removed.	blob \| commitdiff \| raw \| diff to current
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 2	blob \| commitdiff \| raw \| diff to current
2006-12-20	Claudio Sacerdoti...	Bug fixed in cases (it did not produced the right numbe...	blob \| commitdiff \| raw \| diff to current
2006-12-20	Claudio Sacerdoti...	New tactic cases (still to be documented).	blob \| commitdiff \| raw \| diff to current
2006-12-14	Claudio Sacerdoti...	Huge commit:	blob \| commitdiff \| raw \| diff to current
2006-10-23	Claudio Sacerdoti...	CicUniv.UniverseInconsistency is no handled correcly.	blob \| commitdiff \| raw \| diff to current
2006-10-20	Andrea Asperti	This is only a temporary patch. The typecheker raises a	blob \| commitdiff \| raw \| diff to current
2006-09-27	Enrico Tassi	auto snapshot	blob \| commitdiff \| raw \| diff to current
2006-09-27	Claudio Sacerdoti...	One less open helps understanding the code!	blob \| commitdiff \| raw \| diff to current
2006-09-21	Enrico Tassi	apply now uses both menv and subst to decide the fresh...	blob \| commitdiff \| raw \| diff to current
2006-09-04	Enrico Tassi	BIG FAT COMMIT REGARDING COERCIONS:	blob \| commitdiff \| raw \| diff to current
2006-08-29	Ferruccio Guidi	- new tactic subst removes simple non recursive equalit...	blob \| commitdiff \| raw \| diff to current
2006-08-28	Ferruccio Guidi	- Level-1: some fixes to the extraction procedure	blob \| commitdiff \| raw \| diff to current
2006-07-26	Claudio Sacerdoti...	Elim now performs whd to find the inductive type.	blob \| commitdiff \| raw \| diff to current
2006-02-03	Stefano Zacchiroli	- renamed ocaml/ to components/	blob \| commitdiff \| raw \| diff to current

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

RSS Atom