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

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

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

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

2008-07-02	Ferruccio Guidi	- new tactic applyP for use in the Procedural script...	blob \| commitdiff \| raw
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...	Hypotheses patterns for elim implemented. No more need...	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
2007-05-18	Ferruccio Guidi	- new devel contribs/LAMBDA-TYPES/Base-2 with the autom...	blob \| commitdiff \| raw \| diff to current
2007-05-09	Ferruccio Guidi	PrimitiveTactics: intros _ now aveilable	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
2006-12-20	Claudio Sacerdoti...	New tactic cases (still to be documented).	blob \| commitdiff \| raw \| diff to current
2006-09-27	Enrico Tassi	auto snapshot	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-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-06-15	Andrea Asperti	exported 2 functions needed by applyS	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.