| 2005-06-29 |
Enrico Tassi | removed profiling function (now a stub is used instead) |
tree | commitdiff |
| 2005-06-29 |
Claudio Sacerdoti... | Incredible bug of simpl fixed: the stack (in the termin... |
tree | commitdiff |
| 2005-06-29 |
Alberto Griggio | various updates, removed proofs for now because they... |
tree | commitdiff |
| 2005-06-29 |
Ferruccio Guidi | lapply reimplemented using letin_tac |
tree | commitdiff |
| 2005-06-29 |
Claudio Sacerdoti... | does_not_occur unexported since it did not have the... |
tree | commitdiff |
| 2005-06-29 |
Claudio Sacerdoti... | Stupid bug fixed in the refinement of let ... in |
tree | commitdiff |
| 2005-06-28 |
Ferruccio Guidi | lapply improved |
tree | commitdiff |
| 2005-06-28 |
Ferruccio Guidi | lapply improved |
tree | commitdiff |
| 2005-06-28 |
Enrico Tassi | added Drop |
tree | commitdiff |
| 2005-06-28 |
Enrico Tassi | misc -> domMisc |
tree | commitdiff |
| 2005-06-28 |
Claudio Sacerdoti... | New argument for LApply: the ident for the generated... |
tree | commitdiff |
| 2005-06-28 |
Stefano Zacchiroli | changed get_pair interface, now supports different... |
tree | commitdiff |
| 2005-06-28 |
Stefano Zacchiroli | added get_pair method |
tree | commitdiff |
| 2005-06-28 |
Stefano Zacchiroli | moved discovery of METAS dir to configure.ac: script... |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | 1. interface of replace generalized to patterns |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | A few other tactics made available to matita. |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | New argument (the identifier) to generalize. |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | New argument (the hypothesis name) for cut. |
tree | commitdiff |
| 2005-06-27 |
Enrico Tassi | support for _ in binders, and a more coplex pattern... |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | More tactics or tactic arguments made available to... |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | * auto_tac removed (it can be found in CVS) |
tree | commitdiff |
| 2005-06-27 |
Claudio Sacerdoti... | More tactics are now available to matita. |
tree | commitdiff |
| 2005-06-27 |
Enrico Tassi | 1) moved select and pattern_of from cicUtil to proofEng... |
tree | commitdiff |
| 2005-06-27 |
Enrico Tassi | fixed LApply pretty printing |
tree | commitdiff |
| 2005-06-25 |
Ferruccio Guidi | first working (?) version of lapply |
tree | commitdiff |
| 2005-06-25 |
Ferruccio Guidi | firs wrking (?) version of lapply |
tree | commitdiff |
| 2005-06-24 |
Ferruccio Guidi | lapply tactic continued |
tree | commitdiff |
| 2005-06-24 |
Enrico Tassi | new implementation (due to paths). |
tree | commitdiff |
| 2005-06-24 |
Enrico Tassi | stupid rename |
tree | commitdiff |
| 2005-06-24 |
Enrico Tassi | now we use rplace_lifting_csc since the what must NOT... |
tree | commitdiff |
| 2005-06-24 |
Enrico Tassi | fixed select (not Implicit (Some `TYPE) is handled) |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | New implementation of experimental_hint/auto (called... |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | Bug fixed: select => select distinct (since the ors... |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | cicPxpParser.ml*, cicParser2.ml* and cicParser3.ml... |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | Small improvement in extracting suffixes. |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | New functions UriManager.uri_is_var, UriManager.uri_is_con. |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | Asts generalized: a lot of tactics where restricted... |
tree | commitdiff |
| 2005-06-24 |
Claudio Sacerdoti... | debugging printf removed |
tree | commitdiff |
| 2005-06-23 |
Alberto Griggio | added various profiling statistics... |
tree | commitdiff |
| 2005-06-23 |
Enrico Tassi | Much simpler (and slightly more performant) implementat... |
tree | commitdiff |
| 2005-06-23 |
Enrico Tassi | aded prifiler factory |
tree | commitdiff |
| 2005-06-23 |
Claudio Sacerdoti... | The discriminate tactic accepts a term, not only an... |
tree | commitdiff |
| 2005-06-23 |
Claudio Sacerdoti... | Tactic generalize ported to patterns and activated... |
tree | commitdiff |
| 2005-06-23 |
Claudio Sacerdoti... | 1 .Tactic generalize ported to patterns and activated... |
tree | commitdiff |
| 2005-06-22 |
Alberto Griggio | reverted to previous version, as it worked better... |
tree | commitdiff |
| 2005-06-22 |
Stefano Zacchiroli | restored local usage of OCAMLPATH so that ./script... |
tree | commitdiff |
| 2005-06-22 |
Stefano Zacchiroli | added $(NULL) |
tree | commitdiff |
| 2005-06-22 |
Alberto Griggio | use of discrimination trees instead of path indexes... |
tree | commitdiff |
| 2005-06-22 |
Alberto Griggio | trie structure implementation |
tree | commitdiff |
| 2005-06-20 |
Alberto Griggio | some optimizations... |
tree | commitdiff |
| 2005-06-20 |
Alberto Griggio | testing... |
tree | commitdiff |
| 2005-06-20 |
Alberto Griggio | *** empty log message *** |
tree | commitdiff |
| 2005-06-20 |
Alberto Griggio | discrimination trees |
tree | commitdiff |
| 2005-06-19 |
Alberto Griggio | limited-resource-strategy implementation (now working!) |
tree | commitdiff |
| 2005-06-19 |
Alberto Griggio | path indexing integration, limited-resource-strategy... |
tree | commitdiff |
| 2005-06-19 |
Alberto Griggio | path indexing integration |
tree | commitdiff |
| 2005-06-19 |
Alberto Griggio | path indexing working! |
tree | commitdiff |
| 2005-06-17 |
Stefano Zacchiroli | removed! |
tree | commitdiff |
| 2005-06-17 |
Enrico Tassi | added support for goal patterns |
tree | commitdiff |
| 2005-06-17 |
Enrico Tassi | concrete syntax for goal patterns |
tree | commitdiff |
| 2005-06-17 |
Enrico Tassi | added support for patterns current goal |
tree | commitdiff |
| 2005-06-17 |
Enrico Tassi | changed select so that it returns a list of pairs ... |
tree | commitdiff |
| 2005-06-17 |
Alberto Griggio | profiling experiments... |
tree | commitdiff |
| 2005-06-17 |
Claudio Sacerdoti... | more strings to UriManager.uri |
tree | commitdiff |
| 2005-06-17 |
Claudio Sacerdoti... | many strings that are supposed to be URIs are now UriMa... |
tree | commitdiff |
| 2005-06-16 |
Claudio Sacerdoti... | Locally implemented print_context replaced by CicPp... |
tree | commitdiff |
| 2005-06-16 |
Andrea Asperti | A cleaned version of auto_tac_new. |
tree | commitdiff |
| 2005-06-16 |
Stefano Zacchiroli | added depth and width (optional) parameters to auto_tac_new |
tree | commitdiff |
| 2005-06-16 |
Claudio Sacerdoti... | Dead code for packing/unpacking (usually just a big... |
tree | commitdiff |
| 2005-06-16 |
Enrico Tassi | added utility to dump some tables of the db on mowgli |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | DTD for attributes revised. |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | DTD for attributes revised. |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | The `Record class now records also the name of the... |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | Bug fixed: parsing errors were ignored by matitac since... |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | Bug fixed (that used to throw away a metasenv :-( |
tree | commitdiff |
| 2005-06-15 |
Enrico Tassi | fix |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | renamed clientHTTP to http_getter_wget |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | we no longer use pxp |
tree | commitdiff |
| 2005-06-15 |
Ferruccio Guidi | beginning of the tactics lapply and fwd |
tree | commitdiff |
| 2005-06-15 |
Enrico Tassi | apply_tac used to calculate the type of the term before... |
tree | commitdiff |
| 2005-06-15 |
Enrico Tassi | are_convertible on MutCase was no longer checking the... |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | ported to latest registry interface |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | - support for multiple bindings of the same key, access... |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | Refinement of CurrentProof did not check whether the... |
tree | commitdiff |
| 2005-06-15 |
Claudio Sacerdoti... | Big commit and major code clean-up: |
tree | commitdiff |
| 2005-06-15 |
Stefano Zacchiroli | use META helm-registry package, load sample.xml and... |
tree | commitdiff |
| 2005-06-15 |
Alberto Griggio | now something works... |
tree | commitdiff |
| 2005-06-14 |
Claudio Sacerdoti... | * no more %% comments |
tree | commitdiff |
| 2005-06-14 |
Claudio Sacerdoti... | parentheses allowed inside comments |
tree | commitdiff |
| 2005-06-14 |
Claudio Sacerdoti... | test_lexer and test_parser compiled by default |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | uses XmlPushParser instead of PXP |
tree | commitdiff |
| 2005-06-14 |
Enrico Tassi | removed ocaml-pxp |
tree | commitdiff |
| 2005-06-14 |
Enrico Tassi | hack to compile on gazelle |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | done two items |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | don't build pxp (no longer needed), cic_annotations... |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | removed dependencies on Pxp |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | removed dependency on cicPxpParser |
tree | commitdiff |
| 2005-06-14 |
Stefano Zacchiroli | uses XmlPushParser instead of Pxp for parsing getter... |
tree | commitdiff |
| 2005-06-13 |
Stefano Zacchiroli | - no longer build mathql per default |
tree | commitdiff |
| 2005-06-13 |
Enrico Tassi | moved to xmlPushParser |
tree | commitdiff |
| next |
projects / helm.git / history