]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/primitiveTactics.ml
Trick: the refiner always subst-expands the outtype, so that the beta-redex
[helm.git] / helm / software / components / tactics / primitiveTactics.ml
2009-02-03 Enrico Tassicase tactic first tries with a simple outtype and then...
2008-09-26 Enrico Tassilazy proof term to increase sharing and decrease memory...
2008-07-02 Ferruccio Guidi- new tactic applyP for use in the *P*rocedural script...
2008-06-19 Claudio Sacerdoti... 1. bug fixed in generalize_pattern: a lazy const_tac...
2008-06-08 Claudio Sacerdoti... Bug fixed: wrong default pattern for generalize.
2008-06-08 Claudio Sacerdoti... Hypotheses patterns for elim implemented. No more need...
2008-05-30 Enrico TassiCProp hierarchy is there!
2008-04-22 Enrico Tassioblivion ugraph everywhere outside the kernel
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-09 Claudio Sacerdoti... Performance improvement: let-ins should always be pushe...
2007-07-18 Ferruccio Guidithe predicate for elim was not built correctly when...
2007-06-13 Enrico Tassicut is now implemented building a letin and not a beta...
2007-05-18 Ferruccio Guidi- new devel contribs/LAMBDA-TYPES/Base-2 with the autom...
2007-05-17 Enrico Tassiadded a (for the moment) dummy field _subst to Proofeng...
2007-05-09 Ferruccio GuidiPrimitiveTactics: intros _ now aveilable
2007-05-03 Ferruccio Guidielim with a pattern now works correctly (hopefully)
2007-04-27 Andrea AspertiApply_with_subst now returns a subst with a correct...
2007-04-16 Enrico Tassisimplify has a brand new semantics!
2007-04-10 Enrico Tassifixed case
2007-04-10 Enrico Tassiyou can case even if only a right appears... so, substi...
2007-04-04 Ferruccio Guidialpha equivalence test factorized and moved to CicUtil
2007-04-03 Enrico Tassinew case implementation
2007-04-02 Enrico Tassihopefully fixed cases implementation
2007-03-16 Ferruccio Guidielim tactic: it needs two arguments, a term as well...
2007-03-13 Ferruccio Guidielim tactic: now takes a pattern instead of just a...
2007-02-27 Ferruccio Guidi- Procedural: some improvements
2007-02-14 Ferruccio GuidiProcedural : some improvements
2007-02-09 Claudio Sacerdoti... Debugging code removed.
2007-01-10 Ferruccio Guidiattributes now in the proof status: commit 2
2006-12-20 Claudio Sacerdoti... Bug fixed in cases (it did not produced the right numbe...
2006-12-20 Claudio Sacerdoti... New tactic cases (still to be documented).
2006-12-14 Claudio Sacerdoti... Huge commit:
2006-10-23 Claudio Sacerdoti... CicUniv.UniverseInconsistency is no handled correcly.
2006-10-20 Andrea AspertiThis is only a temporary patch. The typecheker raises a
2006-09-27 Enrico Tassiauto snapshot
2006-09-27 Claudio Sacerdoti... One less open helps understanding the code!
2006-09-21 Enrico Tassiapply now uses both menv and subst to decide the fresh...
2006-09-04 Enrico TassiBIG FAT COMMIT REGARDING COERCIONS:
2006-08-29 Ferruccio Guidi- new tactic subst removes simple non recursive equalit...
2006-08-28 Ferruccio Guidi- Level-1: some fixes to the extraction procedure
2006-07-26 Claudio Sacerdoti... Elim now performs whd to find the inductive type.
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/