]> matita.cs.unibo.it Git - helm.git/history - helm/gTopLevel
- debian version 0.0.3-2
[helm.git] / helm / gTopLevel /
2002-11-18 Ferruccio Guidigenerator patched for new semantics with structurated...
2002-11-14 Ferruccio Guidireplaced fun with inverse attribute
2002-11-04 Enrico Tassibug found:
2002-10-31 Ferruccio GuidiMQueryGenerator ported to use fun "objectName"
2002-10-25 Enrico TassiNow esempi/fourier.cic end with a proof!
2002-10-22 Ferruccio GuiditopLevel updated to use mqint set_database and get_database
2002-10-22 Claudio Sacerdoti... Bug ``fixed'': we do not need to apply sym_eqT since...
2002-10-21 Claudio Sacerdoti... No more useful
2002-10-21 natileMerge of the new_mathql branch with the main branch:
2002-10-17 Enrico Tassi- indentation is now in pseudo-functional style!
2002-10-17 Enrico Tassi- rewritesimpl_tac added in fourierR.ml (wrong location)
2002-10-16 Claudio Sacerdoti... - write_tac fixed (the list of new goals was empty)
2002-10-14 Claudio Sacerdoti... A tough test for rewrite.
2002-10-14 Claudio Sacerdoti... - bug fixed: some liftings were missing in the implemen...
2002-10-11 Claudio Sacerdoti... - rewrite extended to handle rewritings with eqT
2002-10-11 Claudio Sacerdoti... Trivial bug in equality_replace fixed: an exception...
2002-10-11 Claudio Sacerdoti... New tactic rewrite implemented.
2002-10-11 Claudio Sacerdoti... - idtac used for debugging removed
2002-10-11 Enrico TassiMore debug printings.
2002-10-10 Enrico TassiAdded an example to test fourier_tac.
2002-10-10 Enrico TassiDebug printing update, now the unification bug
2002-10-09 Claudio Sacerdoti... Several bug-fixes:
2002-10-07 Enrico Tassifourier_tac without useless recursion
2002-10-07 Enrico Tassihopefully last tactic update cvs log
2002-10-02 Enrico Tassitactic update
2002-09-27 Claudio Sacerdoti... Better handling of queries. Now both the locate and...
2002-09-20 Claudio Sacerdoti... change code moved to change_tac (functional version...
2002-09-19 Enrico TassiTactic update
2002-09-18 Claudio Sacerdoti... Small code improvement.
2002-09-18 Enrico TassiTactic update
2002-09-17 Ferruccio Guidinew query generator
2002-09-16 Claudio Sacerdoti... List of tactics implemented and to implement (italian...
2002-09-13 Ferruccio Guidirestricted mode to use when the database is down :)
2002-09-13 Ferruccio Guidiquery generator timing feature improved
2002-09-13 Claudio Sacerdoti... ring.ml* splitted into ring.ml* and tacticals.ml*
2002-09-13 Claudio Sacerdoti... then_ tactical implemented (equivalent to the tclTHEN...
2002-09-13 Enrico TassiFourier tactic update
2002-09-09 Claudio Sacerdoti... When locate is used during the lexing phase, it may...
2002-09-09 Claudio Sacerdoti... Patch applied to the locate query: when used to retriev...
2002-09-09 Enrico TassiFourier tactic update
2002-09-07 Enrico TassiFirst works
2002-09-05 Ferruccio GuidimQueryGenerator and topLevel patched
2002-09-05 Ferruccio Guidisome small improvements: command line sintax changed...
2002-09-04 Claudio Sacerdoti... The parser (the lexer indeed) now use the locate query...
2002-09-04 Enrico TassiFourier tactic
2002-08-29 Michele GalatàType expression simplified.
2002-08-29 Michele GalatàComment typo fixed.
2002-08-27 Claudio Sacerdoti... Interface file created. Missing from previous commit.
2002-07-29 Claudio Sacerdoti... Updated to use the new parser that creates (stacks...
2002-07-22 Claudio Sacerdoti... Many improvements in tactics (and tactical) representation:
2002-07-02 Stefano ZacchiroliAdded examples.
2002-07-02 Stefano Zacchirolibugfix: Ring will work again with varmaps :-)
2002-07-01 Stefano Zacchiroli- added Ring tactic on reals
2002-07-01 Stefano Zacchirolibugfix that inhibit the removal of certain hypotheses
2002-07-01 Stefano Zacchirolibug fix: handled LetIn case in simpl
2002-07-01 Ferruccio GuidimathQL modified, stderr corrected to stdout im mathql_i...
2002-06-25 Claudio Sacerdoti... Locate query changed again. There is a mismatch between...
2002-06-22 Ferruccio Guidited version of mQueryGenerator (was mquery part 2)
2002-06-22 Ferruccio Guidiuntested version of mQueryGenerator (was mquery part 2)
2002-06-19 Claudio Sacerdoti... Bug fixed: a sort not in normal form can now also be...
2002-06-19 Claudio Sacerdoti... Coscoy double inner types now available also for Meta...
2002-06-18 Ferruccio Guidiupdated for the new version of mathQL.ml
2002-06-18 Claudio Sacerdoti... Inner-types a la Coscoy now correctly generated even...
2002-06-18 Claudio Sacerdoti... New query implementation using LetIn.
2002-06-13 Claudio Sacerdoti... Names of some constructors changed.
2002-06-12 Claudio Sacerdoti... * Abst removed from the DTD
2002-06-10 Claudio Sacerdoti... * doubleTypeInference.ml* added. For now, it just compu...
2002-05-29 Claudio Sacerdoti... New module helm-mathql.
2002-05-28 Claudio Sacerdoti... * Bug fixed: syntactic equality for CIC term (which...
2002-05-28 Claudio Sacerdoti... * The "backward" query has been refined considering...
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-22 lordiresult format changed
2002-05-22 Claudio Sacerdoti... Conjectures and Hypotheses inside every conjecture...
2002-05-22 Claudio Sacerdoti... cic2acic.mli added
2002-05-21 Ferruccio Guidi*** empty log message ***
2002-05-20 Claudio Sacerdoti... mathql.ml is now part of ocaml/mathql_interpreter
2002-05-20 Claudio Sacerdoti... mquery.ml now really call the execution of the query.
2002-05-20 Claudio Sacerdoti... Many many improvements:
2002-05-08 Claudio Sacerdoti... Experimental commit: definitions are now allowed in...
2002-04-30 Ferruccio Guidibasic MathQL support
2002-04-29 Claudio Sacerdoti... * Bug fixed: Elim did not work for principles whose...
2002-04-29 Claudio Sacerdoti... * Error handling improved
2002-04-29 Claudio Sacerdoti... Computed inner-types are now also put in whd normal...
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-19 Claudio Sacerdoti... Debugging stuff removed.
2002-04-18 Claudio Sacerdoti... Scratch window is now also raised (= hide + show ;...
2002-04-18 Claudio Sacerdoti... * Error reporting improved
2002-04-18 Claudio Sacerdoti... * Scratch window added
2002-04-18 Claudio Sacerdoti... * Many improvements
2002-04-16 Claudio Sacerdoti... * Many improvements
2002-04-16 Claudio Sacerdoti... Added the possibility to select parts of the goal of...
2002-04-16 Claudio Sacerdoti... Removed the patch to avoid a bug of gmetadom.
2002-04-16 Claudio Sacerdoti... ...
2002-04-16 Claudio Sacerdoti... proofEngineReduction.ml added
2002-04-08 Claudio Sacerdoti... During the computation of the inner-type of a LAMBDA...
next