nCicLibrary

+ config flag added to emove old objects before storing new ones
  I don't even rememberwhy thisisnot done by default

update in ground

+ some renaming

cic notation parser

syntax of constructors updated to match syntax of definitions

milestone update in ground

+ generic relocation maps are now streams of booleans
+ some renaming and restyling
+ operator precedence more uniform
+ recomm updated for relocation

grafite parser updated

+ syntax for parameters added to constructors
  as it was done with definitions some time ago

propagating the arithmetics library, partial commit

+ relocation updated and ported (de Bruijn indexes now start at 1)
+ recomm updated to generate substitution files
+ results on positive integers added to arith
+ some corrections

update in ground

+ notation restyled

update in ground

+ xoa restyled
+ missing files committed

update in gruound

+ library refactored and restyled
+ recomm updated

update in ground

+ arith restyled
+ recomm updated

removing old contribs

+ RELATIONAL: side copies removed
+ developments.txt updated

removing old contribs

+ RELATIONAL
+ ONAG

propagating the arithmetics library, partial commit

+ counters (was: steps) ported and restyled
+ core notation: "pair" decentralized
+ some corrections and renaming

update in bin

+ new application "recomm"
  for restyling comments in λδ source files
+ minor corrections in ground and apps_2

propagating the arithmetics library, partial commit

+ lib ported
+ minor corrections and renaming
+ old parked version of ynat removed

milestone update in ground, partial commit

+ propagating the arithmetics library
+ gathering the arithmetics files
+ function composition respects extensional equivalence
+ minor corrections

arithmetics for λδ

+ arith.ma covered almost in full
+ minor additions and corrections

arithmetics for λδ

+ advances on maximum for non-negative integers
+ part of nat.ma used by λδ covered in full
+ minor additions and corrections

arithmetics for λδ

+ maximum for non-negative integers
+ minor corrections

arithmetics for λδ

strict order for non-ngative integers completed

arithmetics for λδ

+ subtraction for non-negative integers
+ web site update
+ apps_2/examples: minor update

arithmetics for λδ

+ predecessor for non-negative integers
+ web site update

arithmetics for λδ

we rebild the arithmetic library because lib/arithmetics/nat.ma has some problems:
- matitac does not compile it because of known time travel erropr
- too many indexed theorems make the search space explode during auto

λδ site update

+ old references to ground_2 removed
+ Makefile: bugfix

λδ-2B and λδ-ground repackaged for publication

+ web site update

λδ web site update

+ documentation updated

λδ site update

+ another Unicode character sponsored
+ Helena: minor updates
+ Ground: minor updates

update in static_2

one theorem renamed

update in basic_2

+ improved definition of fsb
+ some parked files removed

minor additions to standard library

....

milestone update in basic_2

+ improved rst-transition and related theory
+ minor improvements

update in static_2

+ generic equivalence generalizes syntactic equivalence and sort-irrelevant equivalence
+ minor corrections

decentralized notation in lambda

+ Makefile update

update in staic_2 and basic_2

+ an inversion lemma clarifies the link between rpx and req/reqx/lpx
+ some renaming

update in basic_2

+ rpx_req: cpx_teqx_conf_rex replaced by cpx_teqx_repl_reqx

milestone update in basic_2, update in ground and static_2

+ new definition of cpx and derivatives without the sort hierarchy parameter
+ sort hierarchy parameter removed from ex_fpbg_refl.ma

update in binararies for λδ

+ updated roles
+ some role specifications removed from basic_2A
+ updated web site

renaming in basics/relations

+ we rename adefinition that was clashing with λδ

update in standard library

+ some notations with ^ decentralized
+ one decentralized notation added to reverse_complexity/speedup.ma

ground_2 released and permanently renamed as ground

+ web site update
+ minor corrections

milestone update in ground_2 and basic_2A

+ basic_2A ported to ground_2
+ cpy, cpys and lsuby parked in basic_2A
+ ground_2 updated for basic_2A becomes an independent package
+ ground_2A removed
+ parked files for basic_2A moved in basic_2A
+ web site update

update in binaries for λδ

+ roles: multiple selection and expansion
+ roles: js updated to use multiple selection based on filter
+ roles: option -o
+ roles.osn: wip

update in binaries for λδ

+ roles: updated web interface with filter function in js

update in binaries for λδ

+ roles: updated status allows smarter semantics of option -a
+ roles: bug fixed in option -d
+ roles: improved web interface
+ roles: some typos fixed
+ roles.osn: wip

update in binaries for λδ

+ roles: options -d and -x
+ roles: improved web interface now is usable
+ roles.osn: additions through web interface started

update in binaries for λδ

roles: more transient information in the status
roles: refactored options -o -s -t to -t -n -s

update in binaries for λδ

+ roles: improved web interface
+ roles: -C option improved
+ roles: bug fixed in read_waiting
+ roles.osn regenerated correctly

update in binaries for λδ

roles: WIP ...

update in binaries for λδ

roles: initial infrastructure for the web interface

update in binaries for λδ

roles: options -m, -p and status file update

update in binaries for λδ

roles: option -o and status file update

update in binaries for λδ

roles: option -a and initial status file for λδ

update in basic_2 + new tool "roles"

+ cpg_drops.ma: a proof updated
+ roles: new tool for managing names (-r -s -t -w)
+ names.txt: updated
+ probe: output URI syntax updated

update in lambdadelta

+ probe: name listing with clash analysis
+ lambdadelta: name clashes removed from λδ-2A and λδ-2B

update in lambdadelta

+ sources for λδ-2A added (with a correction)
+ sources for λδ-1A moved
+ λδ-related binaries moved here from web site directory

update in basic_2

+ notation update for cnx and related notions

update in basic_2 and apps_2

+ bug fixed in the notation of cpm and derivatives

update in ground_2, static_2, basic_2

+ refactoring rt-transition counters (rtc)
+ bug fixed in the notation for lifts and drops

update in ground_2, static_2, basic_2, apps_2, alpha_1

+ updated notation with uniform bracket policy
+ notation update for acr
+ some renaming in alpha_1

update in ground_2

+ centralized xoa infrastructure removed
+ unused xoa constructions detected and removed
+ inline: test lines added to Makefile

update in ground_2, static_2, basic_2

+ xoa constructions decentralized in lambdadelta
+ inline: a tool for automatic decentralization of xoa constructions
+ minor bugs fixed

web site update

+ system and specification log completed
+ minor corrections

updated web site

+ updated change log
+ updated site generation procedure

web site update

+ updated generation procedure
+ updated generation software
+ updated css

web site update

+ updated automation for the generated LDDL web site
+ minor improvements

mechanizing the generation of index files for λδ web site

+ initial commit

grundlagen web pages updated

+ some improvements in XSLT processing

λδ web site update

+ changes of λδ-2A vs λδ-1A completed
+ log page linked to site

updated web site

+ new preprint J2a
+ some improvements

web site update

+ some links fixed
+ minor corrections

web site update

+ λδ-2B is released on web site
+ minor corrections

λδ-2B is released

+ some refactoring
+ extra spaces cleaned
+ web site update

update for the article

+ pending conjectures proved
+ some renaming
+ probe: dependences are output in order

update in static_2 and basic_2 for the article

+ commented theorems activated or parked
+ some renaming to match the article

updated probe and matitadep

+ matitadep: bug fixed in loop display
+ new options -b and -i to output backward dependences

update in basic_2

+ t-bound t-computarion for terms
+ validity rules in λδ-2A style justified

update in basic_2

+ cpce parked for now
+ some renaming

update in basic_2

+ new definition of cpce

Merge remote-tracking branch 'origin/ld-0.99.3'

+ renaming

update in basuc_2

+ cpce_drops completed
+ WIP on cpce

Update online helper entries

Fix a wrong message error in 'that is equivalent to' tactic

Add a check on the context of the current proof in 'by induction
hypothesis' tactic

WIP on cpce ...

some added lemmas removed from auto

+ they make auto very slow in some cases,
for instance the /7 width=6 by .../ of contribs/lambdadelta/static_2/relocation/drops.ma

+ WIP on lambdadelta ...

backport of WIP on \lambda\delta to matita 0.99.3

auto tactic of matita 0.99.4 is broken
for now WIP on \lambda\delta continues on this branch

update in ground_2 and basic_2

+ rules for cpt justified
+ cpt is an instance of cpm

Merge remote-tracking branch 'origin/matita-lablgtk3'

matita 0.99.4 now on master branch

update in ground_2 and basic_2

+ initial support for t-transition (the core of inferred type assignment)

matita gtk3: some bugs fixed

+ status#stack is a list of 5 components, not 4
+ removed reference to Stdlib (was Pervasives) to comple with erlier versions of ocaml (ok with 4.0.5)

Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita-lablgtk3

update in static_2

+ notation change for lifts and drops

update in basic_2

+ iterated type assignment completed
+ minor additions to the arith library

debugging code removed

Merge branch 'declarative' into matita-lablgtk3

Change Sort.merge (deprecated) with List.merge

Test pretty printg of declarative tactics

Fix indentation in grafiteAstPp.ml and matitaEnginge.ml with ocp-indent

Add a comment and remove dead code in declarative.ml

Turn off automation weakenings

Generate new .depend files for ng_tactics, syntax_extensions

Add a function that prints a tactic term with the user defined notation
in applyTransformation

Add a function that pretty prints the tactics ASTs to a file while a
script is being parsed and executed

Make 'that is equivalent to' a standalone tactic

Simplify AST types, parsing rules and pp of tactics that had
'that is equivalent to' or 'or equivalently'

Modify grafiteEngine accordingly

Simplify the signature and the code of the implementations of tactics
that had 'that is equivalent to' or 'or equivalently'

A new "volatile_hypo" key is added to the parameter list of the currest
stack level to indicate that the beta rewriting should happen on that
hypothesis, instead of the thesis

Modify beta_rewrite accordingly

Add some "obvious" terms to the given candidates for the automation
(such as refl, sym_eq, trans_eq, etc.)

The weakening of the automation is now only partial: the second flag for
weakening is off. Setting it on makes theorem proving pretty impossible
with the declarative fragment.

Many changes

Add a BetaRewritingStep tactic, for multiple 'or equivalently'
statements in theorems proofs

Remove old code

Add a key-value list to the tiny-cals stack (parameters list) for
context related infos. Can be used as a general purpose store for
key-value pairs

Adapt code that works on the stack to work with the new parameter list

Add function to add and retrieve key-value pairs to the parameters list

Add the concept of volatile-context: they are contexts that are cleared
after the application of some tactics. E.g., the context for a
beta_rewriting (sequence of 'or equivalently') is a volatile context, as
any tactic breaks the chain

Add a function to clear volatile parameters from the paramters list

Add a case in extract_first_goal_from_status for the case where the
stack is empty

Make the tactics that make use of distribute High tactics

Reimplement the dot tac on top of the stack to handle branching. This
makes use of the second iterator list of the stack

Add a "done_continuation" function that checks whether it needs to dot
or recursively merge branches after a done statement

Add a function to push goals from the focus iterator list of the
previous level on the stack to the second iteretaor list of the current
level

Change conclude and obtain to use a volatile context to obligate the
user to only use = inside it

Change the add_names_to_goals function to use the stack instead of the
metasenv directly

Add a unfocus_branch_tac to unfocus from goals in a stack level (useful
for cases and induction)

Change induction and cases to use a context to obligate the user to use
case only inside it. Furthermore, the new stack based branching for
declarative tactics obligates the user to only switch between cases of
the last level

Change induction and cases to start without focusing on any goal and
without automatically focusing on the next goal after a done. The user
is compelled to use case to switch between each case

Change the case to only change case when the current case has been dealt
with

Attempt to fix automation

Add first draft for matita's helper

Fix indentation

Add support for proving cases in a different order

Add some debug pretty printing methods and tactics.

Add a tactic to add names to metasenv goals from a given constructor
list

Modify "we_proceed_by_induction_on" to gather info on the inductive type of
the term being eliminated, apply the right constructor to the right
number of Implicit arguments, and name the new open goals

Modify "we_proceed_by_cases_on" in an analogous way to
"we_proceed_by_induction_on"

Add a tactic to focus on a given case, if present, with helper functions
for it

Modify case to search for the given case and focus on it

Modify indtyinfo to memorize also the costructor list of the inductive
type

Remove a useless if-then-else in index_local_equations2

Remove some old code, comments and trailing spaces

Add last declarative tactics, modify rewriting tactics

Add types for induction and case analysis to grafiteAst. Add new types
for obtain and conclude

Add pp code for induction, case, obtain, conclude

Add calls in grafiteEngine for induction, case, obtain, conclude

Add parsing rules for induction, case, obtain, conclude

Rename a function for code clarity

Add function to swap two goals on the stack (useful for obtain)

Add a conclude function that checks that the given term is the lhs of
the current goal

Add a obtain function that starts an equality chain beginning with the
given term in a new goal

Modify rewriting step to only handle single equality chains steps

Add implementation for induction and case.

Add signatures for induction, case, conclude, obtain

Add keywords to matita.lang for induction, case, conclude, obtain