matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/proofEngineReduction.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/proofEngineReduction.ml

projects / helm.git / history

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

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

2006-01-08	Claudio Sacerdoti...	Added $Id$ to every .ml file.	blob \| commitdiff \| raw
2005-11-27	Stefano Zacchiroli	removed deadcode / fixed typos (thanks to ocaml 3.09)	blob \| commitdiff \| raw \| diff to current
2005-11-08	Claudio Sacerdoti...	Yet another semantics for simplify.	blob \| commitdiff \| raw \| diff to current
2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw \| diff to current
2005-09-05	Claudio Sacerdoti...	Unfold tactic generalized to perform zeta-reduction.	blob \| commitdiff \| raw \| diff to current
2005-09-05	Enrico Tassi	fix generation of applications of applications.	blob \| commitdiff \| raw \| diff to current
2005-09-05	Claudio Sacerdoti...	New strategy for let-in unfolding (aka zeta reduction...	blob \| commitdiff \| raw \| diff to current
2005-07-28	Claudio Sacerdoti...	1. ProofEngineHelpers.locate_in_term, ProofEngineHelper...	blob \| commitdiff \| raw \| diff to current
2005-07-28	Claudio Sacerdoti...	Bug fixed: unfold used to work iff the term to unfold...	blob \| commitdiff \| raw \| diff to current
2005-07-28	Claudio Sacerdoti...	New tactic unfold.	blob \| commitdiff \| raw \| diff to current
2005-06-29	Claudio Sacerdoti...	Incredible bug of simpl fixed: the stack (in the termin...	blob \| commitdiff \| raw \| diff to current
2005-05-24	Enrico Tassi	new simpl semantic (now = and not == since you can...	blob \| commitdiff \| raw \| diff to current
2005-01-21	Stefano Zacchiroli	- attributes support	blob \| commitdiff \| raw \| diff to current
2005-01-17	Enrico Tassi	new cicEnvironment implementation	blob \| commitdiff \| raw \| diff to current
2004-12-01	Enrico Tassi	Added universes handling. The PRE_UNIVERSES tag may...	blob \| commitdiff \| raw \| diff to current
2004-02-06	Stefano Zacchiroli	added annotations to Cic.Implicit	blob \| commitdiff \| raw \| diff to current
2003-09-05	Claudio Sacerdoti...	Defs in context may now have an optional type (when...	blob \| commitdiff \| raw \| diff to current
2003-06-19	Claudio Sacerdoti...	Merge of the V7_3_new_exportation branch.	blob \| commitdiff \| raw \| diff to current

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