| 2005-09-27 |
Stefano Zacchiroli | added/exported pp_pos & pp_attribute
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | removed .annot files (files containing type annotations...
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | more fine grained debug printing
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | changed type of ids_to_uris table to (Cic.id, UriManager...
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | Better handling of idref propagation, no more Href...
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | moved list_uniq to the extlib
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | added support for multiple idrefs
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | added list_uniq
|
commit | commitdiff | tree |
| 2005-09-27 |
Stefano Zacchiroli | completed use of \mod and / notation
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | fixed typo
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | strip heading '\' on Mo s
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | removed some dead code
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | if a node has an xref use it for cut and paste, no...
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | function composition notation
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | div and mod notation ('%' and '\mod')
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | added override for \circ (notation for function composition)
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | added binary version of coq.moo and the corresponding...
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | removed textual version of coq's moo file
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | changed default divide notation to a/b
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | bugfix: reash uris embedded in cic appl patterns
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | - added integrity checks on .moo files
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | better name for a theorem
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | added magic numbers
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | set extlib findlib dependencies
|
commit | commitdiff | tree |
| 2005-09-26 |
Stefano Zacchiroli | implemented the first bunch of useful functions
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | changed .moo format on disk: no longer plain strings...
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | bugfix: evaluation of object commands is now atomic...
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | "verbose" argument of remove is now optional (default...
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | avoid generating useless parens in mathml contextes...
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | removed a line of dead code
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | avoid pattern matching on attributed terms since this...
|
commit | commitdiff | tree |
| 2005-09-23 |
Stefano Zacchiroli | bugfix for uminus notation, prints parens where needed
|
commit | commitdiff | tree |
| 2005-09-21 |
Stefano Zacchiroli | ported to the new parser interface (Ulexing.lexbuf...
|
commit | commitdiff | tree |
| 2005-09-21 |
Stefano Zacchiroli | uses ligatures (as a sample)
|
commit | commitdiff | tree |
| 2005-09-21 |
Stefano Zacchiroli | added ligatures support
|
commit | commitdiff | tree |
| 2005-09-21 |
Stefano Zacchiroli | rebuilt
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | added non-builtin notation for exists
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | changed ast representation of exists
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | pretty printing of literals is now subject to the debug...
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | changed ast representation of exists, now an 'exists...
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | bugfix in default magic handling: consider as having...
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | - bugfix: eta abstractions ignores attributed node...
|
commit | commitdiff | tree |
| 2005-09-20 |
Stefano Zacchiroli | more refere to bindings in env type definition
|
commit | commitdiff | tree |
| 2005-09-19 |
Stefano Zacchiroli | added list.ma
|
commit | commitdiff | tree |
| 2005-09-19 |
Stefano Zacchiroli | - avoid catching top level exceptions when the relevant...
|
commit | commitdiff | tree |
| 2005-09-19 |
Stefano Zacchiroli | splitted command line arguments among debugging and...
|
commit | commitdiff | tree |
| 2005-09-19 |
Stefano Zacchiroli | - added support for -debug, which avoid catching top...
|
commit | commitdiff | tree |
| 2005-09-19 |
Stefano Zacchiroli | - bugfix: when backtracking restore the appropriate...
|
commit | commitdiff | tree |
| 2005-09-16 |
Stefano Zacchiroli | added notation for: nleq, ngeq, nless, and ngtr
|
commit | commitdiff | tree |
| 2005-09-16 |
Stefano Zacchiroli | added notation for nleq, nlgt, ...
|
commit | commitdiff | tree |
| 2005-09-16 |
Stefano Zacchiroli | added entites/overrides for leq, geq, nleq, ngeq, to
|
commit | commitdiff | tree |
| 2005-09-16 |
Stefano Zacchiroli | re-generated
|
commit | commitdiff | tree |
| 2005-09-16 |
Stefano Zacchiroli | uses Hashtbl.replace instead of Hashtbl.add so that:
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | improved discriminate test: check if it works on inductive...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | bugfix in discriminate: now works also with inductive...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | added \neq notation
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | bugfix: save "~" backup together with the non-~ version...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | added -debug flag which avoid catching top-level exception...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | - changed command line interface of cicbrowser so that...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | uniformed ppmetasenv to other pp* methods: substs are...
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | moved matita logo in the right place
|
commit | commitdiff | tree |
| 2005-09-15 |
Stefano Zacchiroli | bugfix: default "false" used to set the _true_ uri ...
|
commit | commitdiff | tree |
| 2005-09-14 |
Stefano Zacchiroli | fixed a finalization issue for connections closed twice
|
commit | commitdiff | tree |
| 2005-09-14 |
Stefano Zacchiroli | done some items
|
commit | commitdiff | tree |
| 2005-09-14 |
Stefano Zacchiroli | added hyperlinks on case pattern heads and outtype
|
commit | commitdiff | tree |
| 2005-09-14 |
Stefano Zacchiroli | enable selections and href handling on elements having...
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | valid baseuri in template
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | no longer use absolute path for naming notebook labels
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | fixed parsing of --x=x ("'uminus" is now right associative)
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | removed a comment/bug report about let..in rendering...
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | fixed "let .. in" rendering, adding the break between...
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | - changed moo representation in MatitaTypes.status...
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | cosmetic changes
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | fixed dummy_floc
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | - fixed dummy_floc (now in DisambiguateTypes)
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | added moo dumping debug item
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | remove matitamake binaries on clean
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | added "commands_of_environment"
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | regenerated
|
commit | commitdiff | tree |
| 2005-09-13 |
Stefano Zacchiroli | moved dummy_floc from Disambiguate to DisambiguateTypes...
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | removed left-spacing of 2 em for '(' (useful only for...
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | - de-ALB-ing
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | cic_textual_parser2 -> cic_disambiguation
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | removed debugging print
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | removed work-arounds for poor disambiguation, which...
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | Added support for multiple disambiguation passes.
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | added support for multi-aliases in disambiguation environment(s)
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | added use_coercions flag (imperative :-(, non re-entrant...
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | - exported CPS iterator visit_magic
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | Filled pre-generated notation levels with productions...
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | done some items
|
commit | commitdiff | tree |
| 2005-09-12 |
Stefano Zacchiroli | commented Record type constructor
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | removed some debugging prints
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | items related to lazy parsing
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | implemented lazy disambiguation of tactics arguments...
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | added set_metasenv on proof_status
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | - uses runtime base dir to reference logo with qed
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | removed some dead code
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | tests changing under a binder
|
commit | commitdiff | tree |
| 2005-09-08 |
Stefano Zacchiroli | uses Map.equal to compare universes
|
commit | commitdiff | tree |
| next |
projects / helm.git / search