]> matita.cs.unibo.it Git - helm.git/history - helm/gTopLevel
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Interface change: only cobj2obj is exposed.
[helm.git] / helm / gTopLevel /
2003-07-20 Claudio Sacerdoti... Cic2acic is now responsible of eta-fixing the objects. tree | commitdiff
2003-07-20 Claudio Sacerdoti... Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc. tree | commitdiff
2003-07-20 Claudio Sacerdoti... Cic2content split into Content and Cic2content. tree | commitdiff
2003-07-18 Andrea AspertiCSC: tentative definition of the ocaml structure that... tree | commitdiff
2003-07-17 Ferruccio Guidi- new generated query "unreferred" implemented at serve... tree | commitdiff
2003-07-16 Claudio Sacerdoti... Xml.token is now namespace-aware. As a consequence... tree | commitdiff
2003-07-16 Andrea AspertiSeveral changes (the beginning of a new era???) tree | commitdiff
2003-07-02 Ferruccio Guidimathql_generator: new constraint format (more type... tree | commitdiff
2003-07-02 Claudio Sacerdoti... Ctr+Backspace is now enabled. Used to perform "alternat... tree | commitdiff
2003-07-02 Claudio Sacerdoti... The editor window now scrolls when the user exceeds... tree | commitdiff
2003-07-01 Claudio Sacerdoti... - DoubleTypeInference.does_not_occur exposed tree | commitdiff
2003-06-30 Claudio Sacerdoti... - default font size of the proof window lowered to 10 tree | commitdiff
2003-06-27 Claudio Sacerdoti... The type of a LetIn is now a LetIn if and only if the... tree | commitdiff
2003-06-27 Claudio Sacerdoti... The "Save proof" menu item is now activated when a... tree | commitdiff
2003-06-27 Claudio Sacerdoti... Reloading bugged stylesheets no longer makes gTopLevel... tree | commitdiff
2003-06-27 Claudio Sacerdoti... Reload stylesheets menu entry added (under the Settings... tree | commitdiff
2003-06-25 Andrea AspertiIt should have already been moved to ocaml/mathql_generator tree | commitdiff
2003-06-25 Claudio Sacerdoti... Removed (it should have already been in ocaml/tactics) tree | commitdiff
2003-06-24 Claudio Sacerdoti... No longer in use. tree | commitdiff
2003-06-20 Ferruccio Guidistyles directory creation now works even if stylesheets... tree | commitdiff
2003-06-20 Claudio Sacerdoti... ... tree | commitdiff
2003-06-20 Claudio Sacerdoti... Installation instructions. tree | commitdiff
2003-06-20 Claudio Sacerdoti... - script.sh added to the repository: you should change... tree | commitdiff
2003-06-19 Claudio Sacerdoti... * mquery_interpreter logging and debugging activated tree | commitdiff
2003-06-19 Claudio Sacerdoti... Merge of the V7_3_new_exportation branch. tree | commitdiff
2002-11-18 Ferruccio Guidigenerator patched for new semantics with structurated... tree | commitdiff
2002-11-14 Ferruccio Guidireplaced fun with inverse attribute tree | commitdiff
2002-11-04 Enrico Tassibug found: tree | commitdiff
2002-10-31 Ferruccio GuidiMQueryGenerator ported to use fun "objectName" tree | commitdiff
2002-10-25 Enrico TassiNow esempi/fourier.cic end with a proof! tree | commitdiff
2002-10-22 Ferruccio GuiditopLevel updated to use mqint set_database and get_database tree | commitdiff
2002-10-22 Claudio Sacerdoti... Bug ``fixed'': we do not need to apply sym_eqT since... tree | commitdiff
2002-10-21 Claudio Sacerdoti... No more useful tree | commitdiff
2002-10-21 natileMerge of the new_mathql branch with the main branch: tree | commitdiff
2002-10-17 Enrico Tassi- indentation is now in pseudo-functional style! tree | commitdiff
2002-10-17 Enrico Tassi- rewritesimpl_tac added in fourierR.ml (wrong location) tree | commitdiff
2002-10-16 Claudio Sacerdoti... - write_tac fixed (the list of new goals was empty) tree | commitdiff
2002-10-14 Claudio Sacerdoti... A tough test for rewrite. tree | commitdiff
2002-10-14 Claudio Sacerdoti... - bug fixed: some liftings were missing in the implemen... tree | commitdiff
2002-10-11 Claudio Sacerdoti... - rewrite extended to handle rewritings with eqT tree | commitdiff
2002-10-11 Claudio Sacerdoti... Trivial bug in equality_replace fixed: an exception... tree | commitdiff
2002-10-11 Claudio Sacerdoti... New tactic rewrite implemented. tree | commitdiff
2002-10-11 Claudio Sacerdoti... - idtac used for debugging removed tree | commitdiff
2002-10-11 Enrico TassiMore debug printings. tree | commitdiff
2002-10-10 Enrico TassiAdded an example to test fourier_tac. tree | commitdiff
2002-10-10 Enrico TassiDebug printing update, now the unification bug tree | commitdiff
2002-10-09 Claudio Sacerdoti... Several bug-fixes: tree | commitdiff
2002-10-07 Enrico Tassifourier_tac without useless recursion tree | commitdiff
2002-10-07 Enrico Tassihopefully last tactic update cvs log tree | commitdiff
2002-10-02 Enrico Tassitactic update tree | commitdiff
2002-09-27 Claudio Sacerdoti... Better handling of queries. Now both the locate and... tree | commitdiff
2002-09-20 Claudio Sacerdoti... change code moved to change_tac (functional version... tree | commitdiff
2002-09-19 Enrico TassiTactic update tree | commitdiff
2002-09-18 Claudio Sacerdoti... Small code improvement. tree | commitdiff
2002-09-18 Enrico TassiTactic update tree | commitdiff
2002-09-17 Ferruccio Guidinew query generator tree | commitdiff
2002-09-16 Claudio Sacerdoti... List of tactics implemented and to implement (italian... tree | commitdiff
2002-09-13 Ferruccio Guidirestricted mode to use when the database is down :) tree | commitdiff
2002-09-13 Ferruccio Guidiquery generator timing feature improved tree | commitdiff
2002-09-13 Claudio Sacerdoti... ring.ml* splitted into ring.ml* and tacticals.ml* tree | commitdiff
2002-09-13 Claudio Sacerdoti... then_ tactical implemented (equivalent to the tclTHEN... tree | commitdiff
2002-09-13 Enrico TassiFourier tactic update tree | commitdiff
2002-09-09 Claudio Sacerdoti... When locate is used during the lexing phase, it may... tree | commitdiff
2002-09-09 Claudio Sacerdoti... Patch applied to the locate query: when used to retriev... tree | commitdiff
2002-09-09 Enrico TassiFourier tactic update tree | commitdiff
2002-09-07 Enrico TassiFirst works tree | commitdiff
2002-09-05 Ferruccio GuidimQueryGenerator and topLevel patched tree | commitdiff
2002-09-05 Ferruccio Guidisome small improvements: command line sintax changed... tree | commitdiff
2002-09-04 Claudio Sacerdoti... The parser (the lexer indeed) now use the locate query... tree | commitdiff
2002-09-04 Enrico TassiFourier tactic tree | commitdiff
2002-08-29 Michele GalatàType expression simplified. tree | commitdiff
2002-08-29 Michele GalatàComment typo fixed. tree | commitdiff
2002-08-27 Claudio Sacerdoti... Interface file created. Missing from previous commit. tree | commitdiff
2002-07-29 Claudio Sacerdoti... Updated to use the new parser that creates (stacks... tree | commitdiff
2002-07-22 Claudio Sacerdoti... Many improvements in tactics (and tactical) representation: tree | commitdiff
2002-07-02 Stefano ZacchiroliAdded examples. tree | commitdiff
2002-07-02 Stefano Zacchirolibugfix: Ring will work again with varmaps :-) tree | commitdiff
2002-07-01 Stefano Zacchiroli- added Ring tactic on reals tree | commitdiff
2002-07-01 Stefano Zacchirolibugfix that inhibit the removal of certain hypotheses tree | commitdiff
2002-07-01 Stefano Zacchirolibug fix: handled LetIn case in simpl tree | commitdiff
2002-07-01 Ferruccio GuidimathQL modified, stderr corrected to stdout im mathql_i... tree | commitdiff
2002-06-25 Claudio Sacerdoti... Locate query changed again. There is a mismatch between... tree | commitdiff
2002-06-22 Ferruccio Guidited version of mQueryGenerator (was mquery part 2) tree | commitdiff
2002-06-22 Ferruccio Guidiuntested version of mQueryGenerator (was mquery part 2) tree | commitdiff
2002-06-19 Claudio Sacerdoti... Bug fixed: a sort not in normal form can now also be... tree | commitdiff
2002-06-19 Claudio Sacerdoti... Coscoy double inner types now available also for Meta... tree | commitdiff
2002-06-18 Ferruccio Guidiupdated for the new version of mathQL.ml tree | commitdiff
2002-06-18 Claudio Sacerdoti... Inner-types a la Coscoy now correctly generated even... tree | commitdiff
2002-06-18 Claudio Sacerdoti... New query implementation using LetIn. tree | commitdiff
2002-06-13 Claudio Sacerdoti... Names of some constructors changed. tree | commitdiff
2002-06-12 Claudio Sacerdoti... * Abst removed from the DTD tree | commitdiff
2002-06-10 Claudio Sacerdoti... * doubleTypeInference.ml* added. For now, it just compu... tree | commitdiff
2002-05-29 Claudio Sacerdoti... New module helm-mathql. tree | commitdiff
2002-05-28 Claudio Sacerdoti... * Bug fixed: syntactic equality for CIC term (which... tree | commitdiff
2002-05-28 Claudio Sacerdoti... * The "backward" query has been refined considering... tree | commitdiff
2002-05-28 Claudio Sacerdoti... Fold must use replace with the = equality and not the... tree | commitdiff
2002-05-24 Claudio Sacerdoti... * Clear and ClearBody implemented, but they are bugged... tree | commitdiff
2002-05-22 lordiresult format changed tree | commitdiff
2002-05-22 Claudio Sacerdoti... Conjectures and Hypotheses inside every conjecture... tree | commitdiff
2002-05-22 Claudio Sacerdoti... cic2acic.mli added tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.