This commit was manufactured by cvs2svn to create tag 'PRE_INDEX_1'.

prima implementazione di demodulate, superposition_left e superposition_right
con gli "indici"...

cambiato il tipo equality, aggiunto l'ordinamento tra left e right

...

test_instance.ma moved to interactive/ (whose tests are not executed for
regression testing)

intro ==> intros

Error message improved.

Now CicMetaSubst.delift_rels restricts the Metas when a failure is faced.
This closes yet another bug in the inference of the outtype for matches.

No more explicit types for the branches of the matches: all the bugs
preventing automatic type inference have been fixed.

snapshot
- almost fully bound SourceView
- started binding of SourceBuffer

CicSubstitution.delift ==> CicMetaSubst.delift_rels
(since it will need to restrict metavariables in case of Rel capture)

lablgtksourceview: first checkin, almost nothing bound ...

Exception raised by delift changed:
Failure ==> DeliftingWouldCaptureAFreeVariable

Debugging code removed.

added debug item for coercion

added \n to "file saved" message

added whd before uri_of_term

removed debug prints

fixed remove_coercion

andrea.ma removed (superseded by match.ma)

Updated to the new syntax for match.

simplified cicBrowser: whelp bar is now always visible

- handles about:* uris in cicBrowser
- added comboboxentry in cicBrowser (still ugly ...)

fixed history handling: now both "home" and link reached via href are
correctly stored and remembered in history

rewritten cicBrowser handling of uri text entry, still some issued with browser
history

The type of a top-level "let rec" can be optional.

Let's try to make the "let rec" construct infer its arguments.

Syntax for top-level "let rec" fixed.

Using the lighter syntax for "let recs".

Using the top-level syntax for let-rec definitions.

The file is now well formed.

New syntax (again) for let rec binders:
let rec f x y (z,w:T) h (c:T) = ...

New lighter syntax for "let rec".

Bug fixed: a symbol must be formed of just one (unicode) character.

Query results were erroneously tagged as directories.

1. syntax of match changed
2. syntax of the bindings of "let rec" made lighter

Yet another bug fixed in the inference of the outtype for match: convertibility
was used in place of unification, making type inference much less powerful
in several useful cases.

The getter maps are now dumped also if matitac exits abruptly.

Added new target "make tests" for regression testing.

Fixed a few bugs in the inference of the outtype for a match.
In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.

Fixed inference of outtype for match when the inductive type has left and/or
right parameters.

Harder test (with empty inductive types and left and right arguments to
inductive types). It does not compile yet.

More informative error message.

clean now also performs clean_metas (since make also creates the metas)

added icons to entries shown in cicbrowser so that directories are
distinguishable from objects

snapshot (minor changes)

* generate list elements in correct order
* handle list inside boxes
* handle box layout
* generate separator between elements (not after elements)

added test for coercions

added coercions

implemented attributes pretty printing

handles "elimCProp" value for class attribute

added object attributes

removed coercions from status

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