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

*** empty log message ***

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

added apply_tac_verbose_with_subst, returning a Cic.substitution instead of a
substitution function, needed by the new paramodulation

added binary version of coq.moo and the corresponding source version

removed textual version of coq's moo file

MatitacleanLib.remove_baseuris will remove empty directories.

permutation.ma added to the repository.

Small bug due to case unsensitiveness in the check function.

changed default divide notation to a/b

bugfix: reash uris embedded in cic appl patterns

- added integrity checks on .moo files
- removed a lot of auxiliary functions from MatitaMisc since they are now part of our extlib

better name for a theorem

added magic numbers
they must be increased each time the data structures dumped in .moo file are changed!!!!

set extlib findlib dependencies

implemented the first bunch of useful functions

Mysql ==> HMysql

New module HMysql (to abstract over Mysql and make profiling easier).

New module HMysql (to abstract over Mysql and make profiling easier).

changed .moo format on disk: no longer plain strings, but ocaml marshalling of GrafiteAst.Command lists

More profiling code.

CicUtil.profile ==> HExtlib.profile

CicUtil.profile ==> HExtlib.profile

...

bugfix: evaluation of object commands is now atomic wrt status (including CicEnvironment, metadata, and the heck ...), either it succeed returning a new status or raises an exception leaving the status unchanged

"verbose" argument of remove is now optional (default false)

Less feedback during removal of objects.

...

Too many OPTIMIZE TABLES (because of a very stupid bug).

save_object_to_disk profiler fixed

Profiling code removed.

several "INSERT VALUE" ==> "INSERT VALUES" (more efficient)

Profiling code removed.

avoid generating useless parens in mathml contextes that do not require them (e.g. exponent, fractions, ...)

removed a line of dead code

Dead code removed again!!!

avoid pattern matching on attributed terms since this loses attributes

fix

universes are saved to disk

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.

added universes list handling

added universes

added parsing of Type:N