fixed some typos

added goals_of_proof

realizability for the induction principle.

added list_concat

added level2 <-> level3 transformations

fixed a bug (status not reset properly between calls), tried some other
euristics (not very satisfactory... :-( )

First draft.

Empty directory.

- added stack frame tagging
- unified "End" for Branch and Select

More informative exceptions raised.

added -nodb support

added support for MATITA_FLAGS and NODB make variables

changed functor interface, now based on proofs instead of metasenvs (this one is implementable on top of ProofEngineTypes ...)

NODB implemented

ignore usual *tex crap

added Makefile

completed instantiatian of level 2 patterns from level 1

bugfix: avoid diversion in "make opt"

- better naming
- uniform handling of empty stack assertion failure
- added Qed and init

first check in of continuationals implementation

in the end: ... proper handling of multiple bindings of the same key, all "set_*" methods now replace the previous binding

bugfix: multiple bindings of the same key work again

completed support for "-nodb", now also matitaclean and its library work with that setting

s/commands_of_domain_and_codomain_items_list/aliases_of_domain_and_codomain_items_list/

added metadata "commands"

uncommented find_cic_appl_pattern_uris

added find

removed debug saving of "foo.conf.xml"

- added support for "-nodb" flag (still missing support for matitaclean which relies on the db)
- centralized parsing of cmdline options in matitaInit. All top level programs which need to parse cmdline will now invoke either MatitaInit.parse_cmdline or MatitaInit.initialize_all and then refer to the relevant keys in the registry
- changed dependencies on hMySql since now it is in a separate library

separated "]]" to avoid clash with (temporary) continuationals ligatures

added MATITA_FLAGS support

rebuilt

added hmysql dependency

- "load_from" no longer clears the previous registry, but instead merge it with loaded key,value pairs
- added "clear" method

rebut

added hmysql

moved hmysql to a separate module

...

aded hmysql/

added filter_map

incomplete snapshot ....

restated ...

Added congruence.ma.

the filled object is inserted in the env after a successful typechecking

Several changes. Proof of Fermat's little theorem completed.

fixed clean_and_fill that now fills the object (used to fill only graph)

moved to fast implementation and fixed a bug in the clean_ugraph function

* well-formedness constraints

* added well-formedness rules for level 2 patterns

* added pattern matching of level 2 terms

- fixed some metasenv issues
- remove closed goals from todo and dot continuations
- use more basic functions for mapping/filtering

fixed some (more) typos

fixed some typos

continuationals semantics: first draft

moved a (commented) test in a handier position

* required for the blob icon

* added concrete syntax for level 2

non-default equalities in equations_for_goal

upgraded code to work with non-default equalities

* snapshot

Further speed-up in the disambiguation algorithm.

The case |choices| = 1 is handled in a special way:
 if |choices| = 1 also for the next ambiguous symbol, then the
  current refinement step is skipped

NOTE: this suggests that pre-setting all the interpretations with cardinality 1
(as it used to be) could greatly speed up things in certain cases

...

* required for texing it

+ well-formedness of level 1 patterns
+ concrete syntax of level 1 patterns
+ level 1 terms

* first version of the specification

better precedence handling, should remove useless parens

New entry: relevant_equations.

spotted missing times notation

fixed some english typos

changed precedence/associativeness handling: relative position of children wrt its (box-)parent is now statically computed starting from the level1 pattern

added/exported pp_pos & pp_attribute

removed .annot files (files containing type annotations generated with ocamlc -dtypes)

small error in nth_prime.

New entry: fermat's little theorem (almost complete).
Corrected plus_to_minus, sparing an hypothesis.

more fine grained debug printing

changed type of ids_to_uris table to (Cic.id, UriManager.uri) Hashtbl.t
(uris are no longer strings)

Better handling of idref propagation, no more Href hack, multiple idrefs are
now kept at the Ast level.
Still issues in idref propagation for magics.

moved list_uniq to the extlib

added support for multiple idrefs

added list_uniq

completed use of \mod and / notation

...

coq.moo is now automatically generated. New targets:
 coq.moo
 coq.moo.opt (almost .PHONY)

fix WE HAVE NO UNIVERSE

fixed typo

./matitaclean all removes all

strip heading '\' on Mo s

removed some dead code

if a node has an xref use it for cut and paste, no matter if it have an href as well

coq.moo is now automatically generated

function composition notation

Coq's existential fixed.

div and mod notation ('%' and '\mod')

added override for \circ (notation for function composition)

matitatop.opt should not be generated

Unification enhanchement.

Unification enhanchement:

 (?1 t) vs (h t)     used to return    ?1 := \lambda x.h x
                     it now returns    ?1 := h

Note: both heuristics are not complete. E.g.:

(H ?1 (?1 t)) vs (H h (h t))                 used to fail (now succeeds)
(H ?1 (?1 t)) vs (H (\lambda x.h x) (h t))   used to succeed (now fails)

Inclusion path fixed.

new signature of auto_tac, with a new optional argument "full", to invoke the
new paramodulation

new paramodulation