added support for coercions

added letin

added syntax for letin

1) Implemented inference of the outtype for empty inductive types
2) The inferred outtype (of non empty ind types) used to omit the lambda abstraction (worked using an amazing feature ot the type checker meant for backward compatibility with Coq 7... ask Claudio).

changed match syntax:
match x in type ty_x with ...

added whd to match argument in guarded_by_destructors;
before only verbatim occurrences of safe variables were accepted.

added Pp of Cast

added integration entry

snapshort
- implemented magic instantiation 2 => 1
- implemented DEFAULT pattern matching compilation 2 => 1

control of dependences improved

*** empty log message ***

My two pennies.

- set monospace buffer using modify_font widget method
- added configuration key for user defined font and built time default

* update

* more to do

* added todo file

snapshot (first version with working pattern matching both 3->2 and 2->1)

yupppppieeeeeeeeeeeeeeeeee!
yayyyy

a contribution about subset theory in an intuitionistic and predicative foundation

snapshot
- regression, but better (and working!) implementation of ML pattern matching
- not yet ported 3 -> 2 pattern matching

... the dunwich horror ...

contribution about \lambda-\delta

snapshot (added typed environment in 2 -> 1 conversion)
... in the eye of the meta-vortex ...
... from Ravenna city

snapshot (first working implementation of parttern matching from level 2
to level 1)

fix_escaping

reduce with path

paths trough terms implemented with a nice hack :)

some cosmetic fixes

fix

removed debug prerr_endline

fixed classical non-C programmer misunderstooding of pointers

fixed intro.

added C.Appl [] case

snapshot (ported to new "typed" ids_to_inner_sort table)

Changed type of ids_to_inner_sort table used in transformation.
It used to be (Cic.id, string) Hashtbl.t, now is (Cic.id, Cic2acic.sort_kind) Hashtbl.t where sort_kind is [ `Type | `Prop | `CProp | `Set ].
String "?", formerly used to denotes meta variable, is not mapped in sort_kind; since it was uniformly treated as "Type", `Type is now used for metas

 added comment

snapshot (first version with [apparently] working mappings between level
2 and level 3)

implemented normalize (used in new_metasenv_for_apply)

fixed width fonts
comments

fixed comments

new shortcuts
fixed hint uri chooser

added colors

snapshot (the thing on the doorstep)

more verbose case failure message

added chronometer

added automathic aliases for _ind _rec and _rect when generated

fix

added automathic aliases for qed and definition

added shortcuts

fix

added uri_of_term

mah...matita.ml

fix

added intros n

added intros n.

added automathic aliases.

- commented out no longer needed macros Redo, Undo, Abort
- bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser
- bugfix: fixed String.sub error on directories shorted than 5 chars

fixed otags invocation

commented out no longer needed macros Redo, Undo, Abort

added %.annot rule to create type annotation files

removed debug prerr_endline

fixed matitac

refactored modules structure

* fold left/right implemented

snapshot
- first version with working DEFAULT magic

1. removed obsolete comments
2. extended delift to the case of meta in head position
3. added a cases (? t1) vs t2: ? gets unified to the beta
expansion of t2 w.r.t t1.

Now the links to 7 pages at a time are shown. Cool.

256 chars max ==> 1024 chars max (because of Coq)

fixed issue with explicit named substitutions

Bugs fixed:
 1. elim did not accept identifiers with "'" in the middle
 2. elim did not accpet URIs

snapshot
- first commit with working list syntax

multiple bindings inside OPT supported

bugfix: "match" now works also when no type is provided for the matched term

let rec example

snapshot (first version in which some extensions work, e.g. infix +)
ueeeeeehh!

some work for Gares

fix

fix

apply now tries both to reduce and to not reduce the applied term

\lambda x.x y ----> \lambda x.(x y)

snapshot
- implemented first draft of extensible parser ... brrrrrr

clean typo

reverted to ==

added .theory check

fixed missing -syntax when using ocamlopt

fixed precedence of \to

added simpl test script

added simpl

fixed syntax

new simpl semantic (now = and not == since you can't write a pointer to a script)

added lost elim_intros_tac

fix

Added a new tactic elim_intros (without simpl of the new goal).

elim -> elim_intros (no simpl)

Added sql/drop_mowgli_tables.mysql.sql

added rule to generate camlp4 expansion of cicNotationParser.ml (in order
to reverse engineer Grammar.extend usage ...)

snapshot

snapshot
- added parse tree for all levels
- implemented parse tree construction for level 1 and 2

fixed clean that wasn't returning the right list of uris owned by the user

added qed

Added andrea.ma

switched to cdbs for debian/rules (now 2 lines long!!!!)