mah...matita.ml

fix

added intros n

added intros n.

added automathic aliases.

- commented out no longer needed macros Redo, Undo, Abort
- bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser
- bugfix: fixed String.sub error on directories shorted than 5 chars

fixed otags invocation

commented out no longer needed macros Redo, Undo, Abort

added %.annot rule to create type annotation files

removed debug prerr_endline

fixed matitac

refactored modules structure

* fold left/right implemented

snapshot
- first version with working DEFAULT magic

1. removed obsolete comments
2. extended delift to the case of meta in head position
3. added a cases (? t1) vs t2: ? gets unified to the beta
expansion of t2 w.r.t t1.

Now the links to 7 pages at a time are shown. Cool.

256 chars max ==> 1024 chars max (because of Coq)

fixed issue with explicit named substitutions

Bugs fixed:
 1. elim did not accept identifiers with "'" in the middle
 2. elim did not accpet URIs

snapshot
- first commit with working list syntax

multiple bindings inside OPT supported

bugfix: "match" now works also when no type is provided for the matched term

let rec example

snapshot (first version in which some extensions work, e.g. infix +)
ueeeeeehh!

some work for Gares

fix

fix

apply now tries both to reduce and to not reduce the applied term

\lambda x.x y ----> \lambda x.(x y)

snapshot
- implemented first draft of extensible parser ... brrrrrr

clean typo

reverted to ==

added .theory check

fixed missing -syntax when using ocamlopt

fixed precedence of \to

added simpl test script

added simpl

fixed syntax

new simpl semantic (now = and not == since you can't write a pointer to a script)

added lost elim_intros_tac

fix

Added a new tactic elim_intros (without simpl of the new goal).

elim -> elim_intros (no simpl)

Added sql/drop_mowgli_tables.mysql.sql

added rule to generate camlp4 expansion of cicNotationParser.ml (in order
to reverse engineer Grammar.extend usage ...)

snapshot

snapshot
- added parse tree for all levels
- implemented parse tree construction for level 1 and 2

fixed clean that wasn't returning the right list of uris owned by the user

added qed

Added andrea.ma

switched to cdbs for debian/rules (now 2 lines long!!!!)

When we unify a Prod against a term t2 which is not a Prod we
now try a whd of t2.

Added a whd on ty in new_metasenv for apply, in order to be able
to apply, e.g. H:(not A) to False.

Hint repaired (an erroneous commit by myself).

fix

added lpo term-ordering

various optimizations (to paramodulation and passive clause selection)

commented out some debugging messages

connected instance to the web search engine

changed debugging code which saves xml input document and input uri so
that it is automatically enabled with debugging

- die on CTRL-C or init.d/... stop instead of resurrecting
- added (commented) debugging code to save xml document

unified grammars and lexers in a single one

fixed some macros, added test_abort.ma

snapshot (implemented level 3 grammar)

fixed some TODO in content2pres

snapshot, notably:
- fixed some lexer bugs
- implemented level 2 patterns grammar

snapshot, notably:
- solved factorization issues in level 1
- support for multiple grammars in cicNotationParser

snapshot

first check-in of cic_notation

fixed whelp bar

fixed Whelp stuff

aded comment

cosmetic changes

bugfix: avoid duplicate entries while indexing (changed implementation
so that sets are internally used everywhere instead of lists, which are
now used only for implementing API)

- cathes more Mysql errors which could happen during post-indexing actions
- bugfix in hits table handling during post-indexing actions
- added copyright info

bugfix in elim, cardinality constraint should >= 1 not > 1

- no longer needs PXP
- added "interpolate" paramater to register iterators

added images

added examples

added comments, fixed history, added loadList to browser

some hacks to make the sequent window pretty nice

fixed instance

added comments

added saturation.opt to the ignore list

fixes (mainly) to demodulation and meta_convertibility

added support for hits table

added list and fill actions

sync script among databases

support hits table

sql for filling hits table

added hits table

better table creator

added "all" table meaning "act on all tables"

fixed

fix bad space

now the extractor manager renames the tables (old tables are renamed to _BACKUP)

some more statements

added index on refRel and the rename table statements

- ported to new ocaml-http API
- uses Arg for cmdline parsing

exported new_metasenv_for_apply, needed by the paramodulation stuff...