]> matita.cs.unibo.it Git - helm.git/history - helm/matita/matitaEngine.ml
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
made executable again
[helm.git] / helm / matita / matitaEngine.ml
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/ commit | commitdiff
2006-01-08 Claudio Sacerdoti... Bug fixed: macros in the middle of a goto cursor or... commit | commitdiff
2006-01-08 Claudio Sacerdoti... Added $Id$ to every .ml file. commit | commitdiff
2006-01-08 Claudio Sacerdoti... 1. Macros are now handled using an execption that is... commit | commitdiff
2005-12-22 Claudio Sacerdoti... Added parameter first_statement_only to the functions... commit | commitdiff
2005-12-22 Claudio Sacerdoti... alias diffing/insertion is now handled by matitaEngine... commit | commitdiff
2005-12-21 Claudio Sacerdoti... Huge reorganization of matita and ocaml. commit | commitdiff
2005-12-07 Enrico TassiBig commit to let Ferruccio try the merge_coercion... commit | commitdiff
2005-12-05 Claudio Sacerdoti... eval_from_stream_greedy finally got rid of! commit | commitdiff
2005-12-05 Claudio Sacerdoti... 1. Several files in grafite that should be in grafite_p... commit | commitdiff
2005-12-03 Claudio Sacerdoti... metadata are no longer stored in .moo files. commit | commitdiff
2005-12-02 Claudio Sacerdoti... 1. matitaEngine splitted into disambiguation (now in... commit | commitdiff
2005-11-30 Claudio Sacerdoti... moved coercions away (work in progress) commit | commitdiff
2005-11-30 Claudio Sacerdoti... Generation of auxiliary lemmas for inductive types... commit | commitdiff
2005-11-29 Claudio Sacerdoti... * Part of matita that used to deal with the library... commit | commitdiff
2005-11-28 Claudio Sacerdoti... DisambiguationError exceptions (that have locations... commit | commitdiff
2005-11-27 Stefano Zacchiroliremoved dead code (thanks to ocaml 3.09) commit | commitdiff
2005-11-26 Claudio Sacerdoti... Experimental localization of errors during refinement... commit | commitdiff
2005-11-24 Stefano ZacchiroliReshaped structure of ocaml/ libraries, matita changed... commit | commitdiff
2005-11-19 Claudio Sacerdoti... Disambiguation errors are no longer thrown away. They... commit | commitdiff
2005-11-18 Enrico Tassifixed coercions undo commit | commitdiff
2005-11-03 Stefano Zacchirolibetter dependencies among modules and symlinking of... commit | commitdiff
2005-10-25 Stefano Zacchirolinew tacticals commit | commitdiff
2005-10-25 Claudio Sacerdoti... Every exception that used to have type string is now... commit | commitdiff
2005-10-17 Enrico Tassiadded coercions to Prod commit | commitdiff
2005-10-05 Stefano Zacchirolicompleted support for "-nodb", now also matitaclean... commit | commitdiff
2005-09-26 Alberto Griggionew signature of auto_tac, with a new optional argument... commit | commitdiff
2005-09-26 Stefano Zacchiroli- added integrity checks on .moo files commit | commitdiff
2005-09-23 Stefano Zacchirolichanged .moo format on disk: no longer plain strings... commit | commitdiff
2005-09-23 Claudio Sacerdoti... CicUtil.profile ==> HExtlib.profile commit | commitdiff
2005-09-23 Stefano Zacchirolibugfix: evaluation of object commands is now atomic... commit | commitdiff
2005-09-23 Enrico Tassiuniverses are saved to disk commit | commitdiff
2005-09-23 Claudio Sacerdoti... The disambiguation now returns the aliases diff. It... commit | commitdiff
2005-09-23 Claudio Sacerdoti... The new_aliases argument of the functions alias_diff... commit | commitdiff
2005-09-21 Stefano Zacchiroliported to the new parser interface (Ulexing.lexbuf... commit | commitdiff
2005-09-19 Claudio Sacerdoti... A bit of profiling functions added here and there. commit | commitdiff
2005-09-16 Enrico Tassiadded a function to reorder the metasenv. commit | commitdiff
2005-09-15 Claudio Sacerdoti... Yet another implementation of the single aliases /... commit | commitdiff
2005-09-15 Stefano Zacchiroli- changed command line interface of cicbrowser so that... commit | commitdiff
2005-09-13 Stefano Zacchiroli- changed moo representation in MatitaTypes.status... commit | commitdiff
2005-09-12 Stefano ZacchiroliAdded support for multiple disambiguation passes. commit | commitdiff
2005-09-08 Stefano Zacchiroliimplemented lazy disambiguation of tactics arguments... commit | commitdiff
2005-09-05 Claudio Sacerdoti... Assert false (for imbricated theorems) changed to a... commit | commitdiff
2005-09-02 Claudio Sacerdoti... Unsharing removed since it is now used in Cic2acic. commit | commitdiff
2005-08-30 Claudio Sacerdoti... A parser for aliases implemented (required by the Whelp). commit | commitdiff
2005-07-29 Claudio Sacerdoti... 0. core_notation.ma splitted into coq.moo and core_nota... commit | commitdiff
2005-07-28 Claudio Sacerdoti... 1. ProofEngineHelpers.locate_in_term, ProofEngineHelper... commit | commitdiff
2005-07-28 Claudio Sacerdoti... New tactic unfold. commit | commitdiff
2005-07-27 Enrico Tassifixed matitamake to handle development with names with... commit | commitdiff
2005-07-22 Alberto Griggioadded optional "paramodulation" parameter to auto to... commit | commitdiff
2005-07-22 Claudio Sacerdoti... Original semantics of a now almost random piece of... commit | commitdiff
2005-07-22 Claudio Sacerdoti... Big changes: commit | commitdiff
2005-07-19 Stefano Zacchirolifixed file descriptor leak commit | commitdiff
2005-07-19 Enrico Tassimessage if the duplicate check may take too long commit | commitdiff
2005-07-19 Enrico Tassimatitac now automatically cleans a non empty baseuri commit | commitdiff
2005-07-19 Ferruccio Guidithe decompose tactic is now working commit | commitdiff
2005-07-18 Stefano Zacchiroliadded too .moo files notation related statements commit | commitdiff
2005-07-18 Stefano Zacchirolimerged cic_notation with matita: good luck! commit | commitdiff
2005-07-15 Enrico Tassimatitamake is integrated with matita commit | commitdiff
2005-07-15 Andrea AspertiBad name should be an error and not just a warning. commit | commitdiff
2005-07-13 Enrico Tassimatitamake stuff: commit | commitdiff
2005-07-11 Enrico Tassiadded a flag to do the check of alredy-proved-theorem commit | commitdiff
2005-07-08 Enrico Tassiadded variant thm flavour commit | commitdiff
2005-07-08 Enrico Tassiadded query commit | commitdiff
2005-07-07 Claudio Sacerdoti... 1. Warnings are now printed in orange (yellow was unvis... commit | commitdiff
2005-07-07 Andrea AspertiRaising an error on a bad theorem name. commit | commitdiff
2005-07-06 Enrico Tassicheck on baseuri commit | commitdiff
2005-07-06 Claudio Sacerdoti... 1. tactical "try_tacticals" renamed to "first" commit | commitdiff
2005-07-05 Ferruccio Guidiname specifications added for elim_intros, elim_intros_... commit | commitdiff
2005-07-05 Enrico Tassinow the moo contains also composed coercions (and It... commit | commitdiff
2005-07-05 Stefano Zacchiroliported to new getter interface commit | commitdiff
2005-07-04 Claudio Sacerdoti... New command default "foo" uri1 ... urin commit | commitdiff
2005-07-04 Claudio Sacerdoti... coercions are now stored in the .moo file. commit | commitdiff
2005-07-04 Claudio Sacerdoti... Use eval_from_stream in place of eval_from_stream_ref... commit | commitdiff
2005-07-04 Claudio Sacerdoti... "include" command implemented. commit | commitdiff
2005-07-04 Claudio Sacerdoti... alias declarations are now put in the .moo file. commit | commitdiff
2005-07-01 Claudio Sacerdoti... Signature of fwdSimpl changed to get rid of a warning. commit | commitdiff
2005-06-30 Claudio Sacerdoti... Signature and concrete syntax of fold fixed. commit | commitdiff
2005-06-30 Ferruccio Guidilapply and fwd improved commit | commitdiff
2005-06-30 Claudio Sacerdoti... 1. rewrite_* and rewrite_back_* merged into one function commit | commitdiff
2005-06-30 Enrico Tassifirst matitadep snapshot commit | commitdiff
2005-06-29 Claudio Sacerdoti... 1. new syntax for patterns: commit | commitdiff
2005-06-29 Enrico Tassinow baseuri is needed in each file (and its redefinitio... commit | commitdiff
2005-06-28 Enrico Tassi* new binary matitatop commit | commitdiff
2005-06-28 Claudio Sacerdoti... New argument for LApply: the ident for the generated... commit | commitdiff
2005-06-27 Claudio Sacerdoti... replace generalized to patterns commit | commitdiff
2005-06-27 Claudio Sacerdoti... A few other tactics made available to matita. commit | commitdiff
2005-06-27 Claudio Sacerdoti... New argument (the identifier) to generalize. commit | commitdiff
2005-06-27 Claudio Sacerdoti... New argument (the hypothesis name) for cut. commit | commitdiff
2005-06-27 Enrico Tassifized disambiguation of LApply commit | commitdiff
2005-06-27 Claudio Sacerdoti... * the auto AST now has the width commit | commitdiff
2005-06-27 Claudio Sacerdoti... * More tactics are now available to matita. commit | commitdiff
2005-06-25 Ferruccio Guidifirst working (?) version of lapply commit | commitdiff
2005-06-24 Ferruccio Guidilapply tactic continued commit | commitdiff
2005-06-24 Claudio Sacerdoti... Asts generalized: a lot of tactics where restricted... commit | commitdiff
2005-06-23 Claudio Sacerdoti... Tactic discriminate activated in matita. commit | commitdiff
2005-06-23 Claudio Sacerdoti... 1. Tactic generalize ported to patterns and activated... commit | commitdiff
2005-06-17 Enrico Tassisupport for goal patterns commit | commitdiff
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri commit | commitdiff
2005-06-16 Stefano Zacchiroliuses auto_tac_new instead of auto_tac commit | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.