added iter_option

"better" (????) identification of assertion failures

Debugging code turned off.

dump_moo added

* More profiling code
* Debugging code restructured

Every exception that used to have type string is now a string Lazy.t.

...

readme file

~subst fixed everywhere in the type-checker:
 1. sometimes it was not passed to functions
 2. sometimes it was passed but it was not used/useful/correct
 3. sometimes it was not passed recursively

t renamed to t' since t was already defined in the same file

Bug fixed: the current substitution and metasenv were not propagated to the
check_allowed_sort_elimination function. As a result:
 1. useless metas were opened by the apply tactic
 2. sometimes unification failed

new semantics, should be the basis for the (re-)implementation

Minor fixings.

Tentative title.

Corrected a mistake in power_upto, and decreased the value of just_factor to
three.

definition of eq improved (?) parametrizing an argument

added coercions to Prod

added some comments; general code cleanup

Added basic bibliography.

more comments added

added few proofs

fixed a couple of bugs that broke tests...

few more cases

tlt_defs: notation updated
ac_defs : PREDICATIVE TOPOLOGY: firs attempt

added few cases

fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

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.