]> matita.cs.unibo.it Git - helm.git/history - helm/gTopLevel/proofEngine.ml
snapshort
[helm.git] / helm / gTopLevel / proofEngine.ml
2005-01-21 Enrico Tassi- sync with the new ApplyTransformation API
2004-11-05 Stefano Zacchiroliported to new cut and letin "API"
2004-11-04 Andrea AspertiPorting to the new version of auto.
2004-11-03 Stefano Zacchirolino longer use Dbi module but directly use Mysql module...
2004-10-22 Stefano Zacchirolitemporary: for the moment we need both MQI handle and...
2004-06-01 Enrico Tassinew universes implementation
2004-05-13 Stefano Zacchirolichanged proofStatus so that uri component is optional...
2004-04-20 Stefano Zacchiroligot rid of ~status label
2004-03-12 acerioniNew tactic Auto.
2004-02-09 Claudio Sacerdoti... Added flag ?eta_fix:bool to acic_object_of_cic_object.
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit
2004-01-22 Stefano Zacchiroliuse new proofEngineHelpers
2003-09-23 Claudio Sacerdoti... ProofEngine.proof is now an abstract data type (since...
2003-06-19 Claudio Sacerdoti... Merge of the V7_3_new_exportation branch.
2002-10-17 Enrico Tassi- rewritesimpl_tac added in fourierR.ml (wrong location)
2002-10-14 Claudio Sacerdoti... - bug fixed: some liftings were missing in the implemen...
2002-10-11 Claudio Sacerdoti... New tactic rewrite implemented.
2002-09-20 Claudio Sacerdoti... change code moved to change_tac (functional version...
2002-09-04 Enrico TassiFourier tactic
2002-07-22 Claudio Sacerdoti... Many improvements in tactics (and tactical) representation:
2002-07-01 Stefano Zacchiroli- added Ring tactic on reals
2002-06-12 Claudio Sacerdoti... * Abst removed from the DTD
2002-05-28 Claudio Sacerdoti... * Bug fixed: syntactic equality for CIC term (which...
2002-05-28 Claudio Sacerdoti... Fold must use replace with the = equality and not the...
2002-05-24 Claudio Sacerdoti... * Clear and ClearBody implemented, but they are bugged...
2002-05-20 Claudio Sacerdoti... Many many improvements:
2002-05-08 Claudio Sacerdoti... Experimental commit: definitions are now allowed in...
2002-04-29 Claudio Sacerdoti... * Bug fixed: Elim did not work for principles whose...
2002-04-26 Claudio Sacerdoti... * Many improvements (expecially in exceptions handling)
2002-04-24 Claudio Sacerdoti... * New implementation of Apply and Elim based on the...
2002-04-19 Claudio Sacerdoti... * The interface of CicTypeChecker now allows the usage...
2002-04-19 Claudio Sacerdoti... Bug fixed: reduction in the scratch window now works...
2002-04-19 Claudio Sacerdoti... Reduction tactics in the scratch window implemented.
2002-04-18 Claudio Sacerdoti... * Many improvements
2002-04-16 Claudio Sacerdoti... * Many improvements
2002-04-08 Claudio Sacerdoti... * Many improvements
2002-04-05 Claudio Sacerdoti... * Many improvements.
2002-04-02 Claudio Sacerdoti... First commit of our future proof-assistant/proof-improv...