| 2004-02-11 |
Claudio Sacerdoti... | Ported to Helm_registry. |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | bugfix: auto_disambiguation is not considered for searc... |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | - script.sh removed from CVS. script.sh.sample added... |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | fixed typo |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | new logger |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | new getter, logger, and the hell |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | new logger, getter, and the hell |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | support for subst |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | new metas (getter's backend, registry, logger, and... |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | ported to new getter (backend) |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | ported to helm registry |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | ported to new logger |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | use debug_print in a debugging message |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | - getter revolution: split backend and frontend (this... |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | - split away gtk logger |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Stefano Zacchiroli | added some debugging messages |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | A type checking error report now prints also the metasenv. |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | added target *.opt (e.g. test.opt, librarytest.opt... |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | - make *opt fixed |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | Big changes: |
commit | commitdiff | tree | snapshot |
| 2004-02-11 |
Claudio Sacerdoti... | Added copyright notice. |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | Explicit Named Substitutions now supported. |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | CicCache ==> CicEnvironment (in testlibrary.ml) |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | - fixed final log reporting (that was broken by one... |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | Bug fixed: when an axiom was asked, an exception was... |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Ferruccio Guidi | patched |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | Only applications whose head was a constant were eta... |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Claudio Sacerdoti... | Bug fixed: checking inductive type declarations with... |
commit | commitdiff | tree | snapshot |
| 2004-02-10 |
Stefano Zacchiroli | added "'" as a valid (continuation) identifier character |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Claudio Sacerdoti... | Added flag ?eta_fix:bool to acic_object_of_cic_object. |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | added thread entry |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | added netstring and pxp deps |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | helm-thread's META |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | thread library (actually contains just ThreadSafe module) |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | - added environment variable overriding |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Claudio Sacerdoti... | sort_of_prod now thinks that a "sort metavariable"... |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Claudio Sacerdoti... | Added is_closed. |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | split into two major parts: |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | bumped version (tag soon) |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | no longer use marshalled table for unicode macros |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Stefano Zacchiroli | use CicAstPp |
commit | commitdiff | tree | snapshot |
| 2004-02-09 |
Claudio Sacerdoti... | eat_prods now uses mk_implicit_type. |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Claudio Sacerdoti... | - Added mk_implicit_sort. |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Claudio Sacerdoti... | Added mk_implicit_sort. |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Claudio Sacerdoti... | A better (but yet not empty) metasenv is now returned. |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Claudio Sacerdoti... | sort_of_prod: the second term, when it is a meta, was... |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Stefano Zacchiroli | - added options "-vars" and "-varsprefix" |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Stefano Zacchiroli | changed deps since testlibrary now uses (minimally... |
commit | commitdiff | tree | snapshot |
| 2004-02-07 |
Stefano Zacchiroli | rebuilt |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Claudio Sacerdoti... | sort metavariables are now generated in an empty canoni... |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | added annotations to Cic.Implicit |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | use ledit for debugging |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Claudio Sacerdoti... | Comments (notes) removed. |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Claudio Sacerdoti... | Code riorganization. |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | added Format-library-friendly pretty printers defined... |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | added -g flag to ocamlc per default |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | textual term editor is now the default one |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | ignore .debug_script (used by Makefile's debug target) |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | - split regtest/testlibrary/gTopLevel objects so that... |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Andrea Asperti | Bug MutCase fixed: now the type of the constructor... |
commit | commitdiff | tree | snapshot |
| 2004-02-06 |
Stefano Zacchiroli | added testlibrary.opt and some cm**** |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | NameExpected exception removed. The "identifier" __n... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | Improved error messages. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | No more garbage in the metasenv. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | New target librarytest (to apply testlibrary.opt to... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | - added support for multiple choices |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | better output format |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | flush stdout after print_string |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | debug prints on stderr |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | removed duplicated entry about freshNamesGenerator |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | - added testlibrary .opts |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | added \to notation for anonymous binders Pi and Lambda |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | bugfix: use rev_uniq also on non-located term |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | sort_of_prod relaxed to accept also Metas (when the... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | - sort_of_prod now returns the second Meta (if it is... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | added html_of_html_msg |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | __n no longer generated. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | "assert false" relaxed to a warning. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | No longer puts anonymous declarations in the canonical... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | - the result of a refinement is now cleared from dummy... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | freshNameGenerator.ml* added |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | rebuilt |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | added freshNameGenerator |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | added testlibrary script |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | use a dummy location when no location is provided |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Stefano Zacchiroli | added ( ) notation for binders |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | dummy dependent types and dummy letins are now removed... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | fresh_name_generator has now also the metasenv parameter. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | mk_fresh_name moved to FreshNamesGenerator. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | New test. |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | Final answer: the local context MUST be normalized... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | Restrict reimplemented to avoid generating lists of... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | Added a TODO (to catch only the right exceptions instea... |
commit | commitdiff | tree | snapshot |
| 2004-02-05 |
Claudio Sacerdoti... | Bug fixed: the canonical contexts were traversed in... |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | Rel to hidden hypotheses are now printed as _hidden_n. |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | ppterm_in_context exported |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | ppcontext (and thus also ppmetasenv) were buggy: the... |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | Functors must be applied using parentheses around the... |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | Added newline. |
commit | commitdiff | tree | snapshot |
| 2004-02-04 |
Claudio Sacerdoti... | Bug fixed: restriction of already restricted contexts... |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog