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.

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