| 2005-07-05 |
Ferruccio Guidi | id ;-) and lapply patched |
tree | commitdiff |
| 2005-07-05 |
Stefano Zacchiroli | ported to new getter interface |
tree | commitdiff |
| 2005-07-05 |
Stefano Zacchiroli | bumped license year |
tree | commitdiff |
| 2005-07-05 |
Stefano Zacchiroli | new getter implementation: no more DBM maps |
tree | commitdiff |
| 2005-07-05 |
Stefano Zacchiroli | handle Not_found exception in extension |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | New command default "foo" uri1 ... urin |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | All the tactics have been ported to use the objects... |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | Comestic changes. |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | Cosmetic changes. |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | New function (only partially implemented) to pretty... |
tree | commitdiff |
| 2005-07-04 |
Stefano Zacchiroli | added some utility functions on filename suffixes |
tree | commitdiff |
| 2005-07-04 |
Claudio Sacerdoti... | "include" command implemented. |
tree | commitdiff |
| 2005-07-02 |
Claudio Sacerdoti... | All the equalityTactics have now been ported to use... |
tree | commitdiff |
| 2005-07-01 |
Alberto Griggio | fixed bug in proof generation, new weight function... |
tree | commitdiff |
| 2005-07-01 |
Enrico Tassi | on is now a keyword (needed in let rec) |
tree | commitdiff |
| 2005-07-01 |
Enrico Tassi | added uri_is_ind |
tree | commitdiff |
| 2005-07-01 |
Alberto Griggio | removed first Cic.term from type equality, added an... |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | TacticAst2Box no longer used. |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | Module TacticAst2Box unused! |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | count_pattern implemented |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | More cases implemented in tactic_count. |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | replace tactic reimplemented. |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | pattern_of function reimplemented. Now it takes a term... |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | prerr_endline -> debug_print |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | The replace tactic is now working again. It can now... |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | Signature of fwdSimpl changed to get rid of a warning. |
tree | commitdiff |
| 2005-07-01 |
Enrico Tassi | uri_of_string now checks the uri is well formed |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | 1. change_tac moved from PrimitiveTactics to ReductionT... |
tree | commitdiff |
| 2005-07-01 |
Claudio Sacerdoti... | Syntax of patterns changed again to make it non-ambiguous: |
tree | commitdiff |
| 2005-06-30 |
Alberto Griggio | proofs are now built lazily at the end of the computation |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | The pattern of a fold cannot have the "wanted" part... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Signature and concrete syntax of fold fixed. |
tree | commitdiff |
| 2005-06-30 |
Ferruccio Guidi | lapply and fwd improved |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | The rewrite_* set of tactics is now working again.... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Bug fixed: a wrong lift made select unuseful when wante... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Pretty printing of Cic.Implict (Some `Hole) is now "%" |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | 1. rewrite_* and rewrite_back_* merged into one function |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Oooops. I forgot the convertibility test that makes... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | The tactic change is now working again. Moreover, it... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | A bit of renaming in the code to make it more clear. |
tree | commitdiff |
| 2005-06-30 |
Enrico Tassi | buri_of_uri is now #xpointer aware. |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Obsolete comment removed. |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | Stupid bug fixed (a completely erroneous assert false... |
tree | commitdiff |
| 2005-06-30 |
Claudio Sacerdoti... | This commit makes ProofEngineHelpers.select reach its... |
tree | commitdiff |
| 2005-06-29 |
Claudio Sacerdoti... | 1. new syntax for patterns: |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history