hack to allow (**)

typo cpying the formal semantic

reorganized guiven_clause to work with the on_the_fly simplification of goals during ghr infer_goals step

demodulation of goal activated again.
to deactivate it, the check_if_goal_set_us_solved should be moved after the infeer_goal step

some experiments

added (but still unused) remove_local_context

added (but not yet used) remove_local_context
weight of non oriented equations decreased

Utils.compare_terms instead of compare_weights
fold_right -> fold_right

occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
considered the same.

...

- some fixes regarding URIs of equality that now should be coherent with the
  one of the goal
- eliminated the stack overflow issue when building the proof

instead of including library_notation we include logic/equality that is smaller

fix

contribution on relational arithmetics started

fixed

fixes

ecco le gatte da pelare

ancient bug solved. if the term is (eq TY A B) the signature of A and B was
ignored if TY was a Sort.

some more on equalities

added log.120.orsay.txt and comparison

some examples of the new ApplyS tactic

examples of applyS

Apply-Silvie tactic added!

added applyS

some fixed done in Orsay:
- supL is called on both sides if the equation is not oriented
- contextualize_rewrites fixed if multiple equalities are used (equalities on different types)

exported 2 functions needed by applyS

...

default constants are now the matita standard library ones and not the one from Coq.
the makefile should work on every checkout, since the path for the TPTP stuff is not hardcoded, but ppoint to the TPTP-VERSION/ directory in the user's home.

bumped date

center figures in HTML version of the manual using CSS

changed install target so that figures are instaled as well

fixed bad spellend "stantard"

removed old ignore lines about matita.conf.xml.ROLE

Enrico: bugfix, remove depend.errors upon destroy

removed old debugging print

relocation of developments.png

adding the developments screenshot

bumped date

typo: titleabbrev stuff should not be bold

added generation of quick reference card of tactic syntax

- distributed matitaGeneratedGui.ml (needed)
- when distributed 'world' is the default target

generate gui code upon distribution

distribute more stuff
added an install target to the manual makefile

reordered author list

updated some distributed stuff

recursive invocation of distr_pre

filled README, BUGS, and other files useful for the distribution

moved benchmnarks/ dir outside of components/

added shortcut targets

added dummy <entry /> to make yelp happy

- better formatting/factorization of tables used for grammar description
- improved rendering toward TeX

- slight fix in lapply syntax
- Ferruccio Guidi is NOT a former member :)

generate deps on the fly
added dep on the stylesheets

removed overkilling info for our manual

consistent naming of the calculus

css stylesheets for the on-line manual

factorized legal stuff like other chapters

new documentation for the decompose tactic

More documentation committed.

Syntactic bug changed: t in "unfold t" must be a tactic_term, not a term

Tactics are now documented using bolds for terminal symbols.

1. the default for the default equality/absurd/true/false URIs used to be
   the Coq ones; now it is None
2. legacy/coq.ma changed to set the default URIs for Coq
3. generation of inversion principles is now branched again

[a-z] syntax documented

Lexical conventions documented.

Notation for congruent.
Restyling of fermat's little theorem with tynicals.

the Matita manual is now convertible to a decent .tex that is processable both
by latex and pdflatex, changes involved:
- use the 'unicode' latex package.  The unicode package, being quite large, has
  been imported under trunk/software/share/texmf/unicode
- added the definition of mappings from some unicode symbol we use (and which
  are not defined in the default unicode package) to tex macros. See
  share/texmf/unicode/config/matita.ucf
- added some parameters to the stylesheet used to generate .tex from .xml

developments added

added "dumb" test target

Attempt to make our markup respect the docbook specification(!), major changes
required:
1) added <para> wrappers where missing
2) added titles to tables
3) removed empty <thead> elements
Point (3) make yelp now shows rules in tables used for syntax references. IMO
this not a good reason to have empty <thead> elements, since they violates the
docbook DTDs. Either yelp should be fixed to not ignore frame/rowsep/colsep
attributes (as it currently does) or we need to find a different markup for
displaying EBNF like grammars.

bug fixed in doc

(co)inductive type declarations are now documented

Record syntax is now described.
More &TODO; put here and there.

implemented tinycals:
- 1,2,3: ...
- *:

commented the finally function

fix

...

...

use the appropriate chain of transormations for pretty printing term

made pp_term parametric and explained the proper way of solving the object pretty printing problem

Bug fixed that made theory rendering bugged after visiting a whelp search page.

bugfix: rely on byte count instead of mixing byte and character count

Subsumption_subst must be applied to the initial proof before passing
it to build_proof_goal.

Sigma algebras and measurable maps defined.

Committed a first experiment in the formalization of Lebesgue dominated
convergence theorem: basic set theory and classical topology definitions.

\n restored

fixed proofs, contextualization should now work.
the empty context is not a term with an open (Rel 1), but a
a term with a (Cic.Implicit(Some `Hole)) so that it can't bw confused with a
Rel to the last Hypothesis.

1. the default encoding for the stylesheets is now UTF8
2. committed a few changes in search.xsl that had never been committed before

matita.txt updated

Bug fixed: theories were handled as base uris, not as uris of files.

letin are now sorted properly.

fixed proof generation again

use the proper top level function to parse terms

ZACK: export a top level function for parsing terms, it can't be bypassed due to the Obj.magic trick

...

A -> Univ

canonical and contextualize_rewrites are back, they seem to work now...

the function to create on the fly a symmetry step has been moved to equality

added our poor results to CASC 2005

ZACK: ported to the latest ocaml-http API

ZACK: ported to the latest ocaml-http API