2004-02-20 |
Stefano Zacchiroli | bugfix: "in" is an IDENT, not a keyword |
tree | commitdiff |
2004-02-20 |
Ferruccio Guidi | hard-coded timing of generated queries disabled: use... |
tree | commitdiff |
2004-02-20 |
Ferruccio Guidi | - mathql interpreter flags reorganized |
tree | commitdiff |
2004-02-19 |
Ferruccio Guidi | source logging patched |
tree | commitdiff |
2004-02-19 |
Ferruccio Guidi | source logging is now native in the interpreter |
tree | commitdiff |
2004-02-19 |
Ferruccio Guidi | source logging enabled by default |
tree | commitdiff |
2004-02-19 |
Andrea Asperti | Adding tacticAst2Box (pretty printer for tactical,... |
tree | commitdiff |
2004-02-19 |
Andrea Asperti | Minor modification in test_parser (to use the new prett... |
tree | commitdiff |
2004-02-18 |
Ferruccio Guidi | mathql interpreter flags can be now red from helm registry |
tree | commitdiff |
2004-02-18 |
Claudio Sacerdoti... | helm_registry is already in due to transitive dependencies |
tree | commitdiff |
2004-02-18 |
Claudio Sacerdoti... | The order IS significative. Changing the order (in... |
tree | commitdiff |
2004-02-18 |
Claudio Sacerdoti... | typo fixed. Used to break the ls method. |
tree | commitdiff |
2004-02-18 |
Stefano Zacchiroli | fixed cosmetic typos during pretty printing |
tree | commitdiff |
2004-02-18 |
Stefano Zacchiroli | - bugfix in term grammar: lowered precedence level... |
tree | commitdiff |
2004-02-18 |
Stefano Zacchiroli | catch parse error exception and show them to the user... |
tree | commitdiff |
2004-02-18 |
Ferruccio Guidi | patched |
tree | commitdiff |
2004-02-18 |
Claudio Sacerdoti... | Bug fixed: Helm_registry was used not enough lazily... |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | added copyright info |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | removed useless Mpresentation module |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | moved away tactics and tacticals |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | added tactics and tacticals (heavily bugged) |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | added hook for .cma link time options |
tree | commitdiff |
2004-02-17 |
Stefano Zacchiroli | added tactic and tactical (still heavily bugged!!!) |
tree | commitdiff |
2004-02-17 |
Claudio Sacerdoti... | The PostgreSQL connection string has been moved to... |
tree | commitdiff |
2004-02-17 |
Claudio Sacerdoti... | Porting of applyStylesheets.ml to Helm_registry. |
tree | commitdiff |
2004-02-17 |
Claudio Sacerdoti... | mathql_db_map.txt is now retrieved by Helm_registry. |
tree | commitdiff |
2004-02-17 |
Claudio Sacerdoti... | -linkall removed |
tree | commitdiff |
2004-02-17 |
Claudio Sacerdoti... | - double_type_of: sort_of_prod modified to expect also... |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | bugfix: top level keys now should work |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | - more structured configuration file |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | added ocamlinit target which creates a .ocamlinit file |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | solved a precedence issue between binders and arrows |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | do not use tex notation per default (used only by tex... |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | use BoxPp |
tree | commitdiff |
2004-02-16 |
Stefano Zacchiroli | - added arrow notation |
tree | commitdiff |
2004-02-13 |
Stefano Zacchiroli | inductive type ident optional in mutcase |
tree | commitdiff |
2004-02-13 |
Stefano Zacchiroli | s/pcre/str/ |
tree | commitdiff |
2004-02-13 |
Andrea Asperti | new (box based) pretty printer |
tree | commitdiff |
2004-02-13 |
Stefano Zacchiroli | split configure.ac in two parts: ocaml and gTopLevel |
tree | commitdiff |
2004-02-13 |
Stefano Zacchiroli | - added support for variable interpolation |
tree | commitdiff |
2004-02-12 |
Ferruccio Guidi | patched for *.cmx |
tree | commitdiff |
2004-02-12 |
Ferruccio Guidi | new .depend files |
tree | commitdiff |
2004-02-12 |
Stefano Zacchiroli | removed some anciente debugging messages |
tree | commitdiff |
2004-02-12 |
Claudio Sacerdoti... | libraries-complete.ps: |
tree | commitdiff |
2004-02-12 |
Claudio Sacerdoti... | libraries-complete.ps: the internal libraries are now... |
tree | commitdiff |
2004-02-12 |
Claudio Sacerdoti... | Added new target libraries-complete.ps (with also all... |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | fixed typo |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | new logger |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | new logger, getter, and the hell |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | support for subst |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | new metas (getter's backend, registry, logger, and... |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | ported to new getter (backend) |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | ported to helm registry |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | ported to new logger |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | use debug_print in a debugging message |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | - getter revolution: split backend and frontend (this... |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | - split away gtk logger |
tree | commitdiff |
2004-02-11 |
Stefano Zacchiroli | added some debugging messages |
tree | commitdiff |
2004-02-11 |
Claudio Sacerdoti... | A type checking error report now prints also the metasenv. |
tree | commitdiff |
2004-02-11 |
Claudio Sacerdoti... | Big changes: |
tree | commitdiff |
2004-02-11 |
Claudio Sacerdoti... | Added copyright notice. |
tree | commitdiff |
2004-02-10 |
Claudio Sacerdoti... | Explicit Named Substitutions now supported. |
tree | commitdiff |
2004-02-10 |
Claudio Sacerdoti... | Bug fixed: when an axiom was asked, an exception was... |
tree | commitdiff |
2004-02-10 |
Claudio Sacerdoti... | Only applications whose head was a constant were eta... |
tree | commitdiff |
2004-02-10 |
Claudio Sacerdoti... | Bug fixed: checking inductive type declarations with... |
tree | commitdiff |
2004-02-10 |
Stefano Zacchiroli | added "'" as a valid (continuation) identifier character |
tree | commitdiff |
2004-02-09 |
Claudio Sacerdoti... | Added flag ?eta_fix:bool to acic_object_of_cic_object. |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | added thread entry |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | added netstring and pxp deps |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | helm-thread's META |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | thread library (actually contains just ThreadSafe module) |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | - added environment variable overriding |
tree | commitdiff |
2004-02-09 |
Claudio Sacerdoti... | sort_of_prod now thinks that a "sort metavariable"... |
tree | commitdiff |
2004-02-09 |
Claudio Sacerdoti... | Added is_closed. |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | no longer use marshalled table for unicode macros |
tree | commitdiff |
2004-02-09 |
Stefano Zacchiroli | use CicAstPp |
tree | commitdiff |
2004-02-09 |
Claudio Sacerdoti... | eat_prods now uses mk_implicit_type. |
tree | commitdiff |
2004-02-07 |
Claudio Sacerdoti... | - Added mk_implicit_sort. |
tree | commitdiff |
2004-02-07 |
Claudio Sacerdoti... | Added mk_implicit_sort. |
tree | commitdiff |
2004-02-07 |
Claudio Sacerdoti... | sort_of_prod: the second term, when it is a meta, was... |
tree | commitdiff |
2004-02-06 |
Claudio Sacerdoti... | sort metavariables are now generated in an empty canoni... |
tree | commitdiff |
2004-02-06 |
Stefano Zacchiroli | added annotations to Cic.Implicit |
tree | commitdiff |
2004-02-06 |
Claudio Sacerdoti... | Comments (notes) removed. |
tree | commitdiff |
2004-02-06 |
Claudio Sacerdoti... | Code riorganization. |
tree | commitdiff |
2004-02-06 |
Stefano Zacchiroli | added Format-library-friendly pretty printers defined... |
tree | commitdiff |
2004-02-06 |
Stefano Zacchiroli | added -g flag to ocamlc per default |
tree | commitdiff |
2004-02-06 |
Stefano Zacchiroli | textual term editor is now the default one |
tree | commitdiff |
2004-02-06 |
Andrea Asperti | Bug MutCase fixed: now the type of the constructor... |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | NameExpected exception removed. The "identifier" __n... |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | Improved error messages. |
tree | commitdiff |
2004-02-05 |
Stefano Zacchiroli | debug prints on stderr |
tree | commitdiff |
2004-02-05 |
Stefano Zacchiroli | removed duplicated entry about freshNamesGenerator |
tree | commitdiff |
2004-02-05 |
Stefano Zacchiroli | added \to notation for anonymous binders Pi and Lambda |
tree | commitdiff |
2004-02-05 |
Stefano Zacchiroli | bugfix: use rev_uniq also on non-located term |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | sort_of_prod relaxed to accept also Metas (when the... |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | - sort_of_prod now returns the second Meta (if it is... |
tree | commitdiff |
2004-02-05 |
Stefano Zacchiroli | added html_of_html_msg |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | "assert false" relaxed to a warning. |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | No longer puts anonymous declarations in the canonical... |
tree | commitdiff |
2004-02-05 |
Claudio Sacerdoti... | - the result of a refinement is now cleared from dummy... |
tree | commitdiff |
next |