]> matita.cs.unibo.it Git - helm.git/log
helm.git
4 years agoupdate in basic_2
Ferruccio Guidi [Sun, 27 Sep 2020 12:01:04 +0000 (14:01 +0200)]
update in basic_2

+ improved definition of fsb
+ some parked files removed

4 years agominor additions to standard library
Ferruccio Guidi [Fri, 25 Sep 2020 21:56:49 +0000 (23:56 +0200)]
minor additions to standard library

....

4 years agomilestone update in basic_2
Ferruccio Guidi [Fri, 25 Sep 2020 21:54:50 +0000 (23:54 +0200)]
milestone update in basic_2

+ improved rst-transition and related theory
+ minor improvements

4 years agoupdate in static_2
Ferruccio Guidi [Sat, 18 Jul 2020 18:49:45 +0000 (20:49 +0200)]
update in static_2

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

4 years agodecentralized notation in lambda
Ferruccio Guidi [Thu, 30 Apr 2020 20:32:06 +0000 (22:32 +0200)]
decentralized notation in lambda

+ Makefile update

4 years agoupdate in staic_2 and basic_2
Ferruccio Guidi [Fri, 24 Apr 2020 21:27:24 +0000 (23:27 +0200)]
update in staic_2 and basic_2

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

4 years agoupdate in basic_2
Ferruccio Guidi [Tue, 21 Apr 2020 12:35:09 +0000 (14:35 +0200)]
update in basic_2

+ rpx_req: cpx_teqx_conf_rex replaced by cpx_teqx_repl_reqx

4 years agomilestone update in basic_2, update in ground and static_2
Ferruccio Guidi [Thu, 16 Apr 2020 16:13:01 +0000 (18:13 +0200)]
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

4 years agoupdate in binararies for λδ
Ferruccio Guidi [Thu, 9 Apr 2020 17:26:31 +0000 (19:26 +0200)]
update in binararies for λδ

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

4 years agorenaming in basics/relations
Ferruccio Guidi [Thu, 9 Apr 2020 13:52:50 +0000 (15:52 +0200)]
renaming in basics/relations

+ we rename adefinition that was clashing with λδ

4 years agoupdate in standard library
Ferruccio Guidi [Thu, 5 Mar 2020 14:16:35 +0000 (15:16 +0100)]
update in standard library

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

4 years agoground_2 released and permanently renamed as ground
Ferruccio Guidi [Thu, 27 Feb 2020 21:45:50 +0000 (22:45 +0100)]
ground_2 released and permanently renamed as ground

+ web site update
+ minor corrections

4 years agomilestone update in ground_2 and basic_2A
Ferruccio Guidi [Thu, 27 Feb 2020 15:18:06 +0000 (16:18 +0100)]
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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Mon, 17 Feb 2020 20:25:02 +0000 (21:25 +0100)]
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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Tue, 11 Feb 2020 18:35:15 +0000 (19:35 +0100)]
update in binaries for λδ

+ roles: updated web interface with filter function in js

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Mon, 10 Feb 2020 11:17:42 +0000 (12:17 +0100)]
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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Sat, 8 Feb 2020 08:46:44 +0000 (09:46 +0100)]
update in binaries for λδ

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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Fri, 7 Feb 2020 12:44:42 +0000 (13:44 +0100)]
update in binaries for λδ

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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Thu, 6 Feb 2020 10:37:08 +0000 (11:37 +0100)]
update in binaries for λδ

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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Mon, 3 Feb 2020 23:31:54 +0000 (00:31 +0100)]
update in binaries for λδ

roles: WIP ...

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Fri, 31 Jan 2020 20:12:57 +0000 (21:12 +0100)]
update in binaries for λδ

roles: initial infrastructure for the web interface

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Thu, 30 Jan 2020 15:21:11 +0000 (16:21 +0100)]
update in binaries for λδ

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

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Thu, 30 Jan 2020 12:15:20 +0000 (13:15 +0100)]
update in binaries for λδ

roles: option -o and status file update

4 years agoupdate in binaries for λδ
Ferruccio Guidi [Wed, 29 Jan 2020 16:25:47 +0000 (17:25 +0100)]
update in binaries for λδ

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

4 years agoupdate in basic_2 + new tool "roles"
Ferruccio Guidi [Sat, 25 Jan 2020 21:36:39 +0000 (22:36 +0100)]
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

4 years agoupdate in lambdadelta
Ferruccio Guidi [Sat, 18 Jan 2020 22:20:28 +0000 (23:20 +0100)]
update in lambdadelta

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

4 years agoupdate in lambdadelta
Ferruccio Guidi [Fri, 17 Jan 2020 13:50:17 +0000 (14:50 +0100)]
update in lambdadelta

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

4 years agoupdate in basic_2
Ferruccio Guidi [Wed, 15 Jan 2020 19:22:26 +0000 (20:22 +0100)]
update in basic_2

+ notation update for cnx and related notions

4 years agoupdate in basic_2 and apps_2
Ferruccio Guidi [Tue, 14 Jan 2020 18:08:54 +0000 (19:08 +0100)]
update in basic_2 and apps_2

+ bug fixed in the notation of cpm and derivatives

4 years agoupdate in ground_2, static_2, basic_2
Ferruccio Guidi [Fri, 10 Jan 2020 11:44:18 +0000 (12:44 +0100)]
update in ground_2, static_2, basic_2

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

4 years agoupdate in ground_2, static_2, basic_2, apps_2, alpha_1
Ferruccio Guidi [Wed, 8 Jan 2020 21:39:47 +0000 (22:39 +0100)]
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

4 years agoupdate in ground_2
Ferruccio Guidi [Mon, 6 Jan 2020 21:13:52 +0000 (22:13 +0100)]
update in ground_2

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

4 years agoupdate in ground_2, static_2, basic_2
Ferruccio Guidi [Mon, 6 Jan 2020 17:13:12 +0000 (18:13 +0100)]
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

4 years agoweb site update
Ferruccio Guidi [Fri, 20 Dec 2019 17:44:34 +0000 (18:44 +0100)]
web site update

+ system and specification log completed
+ minor corrections

4 years agoupdated web site
Ferruccio Guidi [Thu, 19 Dec 2019 16:16:44 +0000 (17:16 +0100)]
updated web site

+ updated change log
+ updated site generation procedure

4 years agoweb site update
Ferruccio Guidi [Sat, 14 Dec 2019 11:22:13 +0000 (12:22 +0100)]
web site update

+ updated generation procedure
+ updated generation software
+ updated css

4 years agoweb site update
Ferruccio Guidi [Wed, 11 Dec 2019 22:40:24 +0000 (23:40 +0100)]
web site update

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

4 years agomechanizing the generation of index files for λδ web site
Ferruccio Guidi [Mon, 9 Dec 2019 23:24:30 +0000 (00:24 +0100)]
mechanizing the generation of index files for λδ web site

+ initial commit

4 years agogrundlagen web pages updated
Ferruccio Guidi [Mon, 9 Dec 2019 19:38:48 +0000 (20:38 +0100)]
grundlagen web pages updated

+ some improvements in XSLT processing

4 years agoλδ web site update
Ferruccio Guidi [Fri, 6 Dec 2019 21:10:54 +0000 (22:10 +0100)]
λδ web site update

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

4 years agoupdated web site
Ferruccio Guidi [Mon, 2 Dec 2019 12:42:43 +0000 (13:42 +0100)]
updated web site

+ new preprint J2a
+ some improvements

5 years agoweb site update
Ferruccio Guidi [Thu, 21 Nov 2019 23:12:52 +0000 (00:12 +0100)]
web site update

+ some links fixed
+ minor corrections

5 years agoweb site update
Ferruccio Guidi [Wed, 20 Nov 2019 18:08:07 +0000 (19:08 +0100)]
web site update

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

5 years agoλδ-2B is released
Ferruccio Guidi [Tue, 19 Nov 2019 19:45:15 +0000 (20:45 +0100)]
λδ-2B is released

+ some refactoring
+ extra spaces cleaned
+ web site update

5 years agoupdate for the article
Ferruccio Guidi [Mon, 18 Nov 2019 22:12:40 +0000 (23:12 +0100)]
update for the article

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

5 years agoupdate in static_2 and basic_2 for the article
Ferruccio Guidi [Fri, 15 Nov 2019 15:22:29 +0000 (16:22 +0100)]
update in static_2 and basic_2 for the article

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

5 years agoupdated probe and matitadep
Ferruccio Guidi [Sat, 9 Nov 2019 17:27:55 +0000 (18:27 +0100)]
updated probe and matitadep

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

5 years agoupdate in basic_2
Ferruccio Guidi [Mon, 28 Oct 2019 19:37:33 +0000 (20:37 +0100)]
update in basic_2

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

5 years agoupdate in basic_2
Ferruccio Guidi [Fri, 25 Oct 2019 15:59:07 +0000 (17:59 +0200)]
update in basic_2

+ cpce parked for now
+ some renaming

5 years agoupdate in basic_2
Ferruccio Guidi [Mon, 21 Oct 2019 16:35:57 +0000 (18:35 +0200)]
update in basic_2

+ new definition of cpce

5 years agoMerge remote-tracking branch 'origin/ld-0.99.3'
Ferruccio Guidi [Fri, 18 Oct 2019 14:39:15 +0000 (16:39 +0200)]
Merge remote-tracking branch 'origin/ld-0.99.3'

+ renaming

5 years agoupdate in basuc_2 ld-0.99.3
Ferruccio Guidi [Thu, 17 Oct 2019 15:20:58 +0000 (17:20 +0200)]
update in basuc_2

+ cpce_drops completed
+ WIP on cpce

5 years agoUpdate online helper entries
Claudio Sacerdoti Coen [Wed, 16 Oct 2019 07:06:34 +0000 (09:06 +0200)]
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

5 years agoWIP on cpce ...
Ferruccio Guidi [Mon, 14 Oct 2019 21:44:24 +0000 (23:44 +0200)]
WIP on cpce ...

5 years agosome added lemmas removed from auto
Ferruccio Guidi [Mon, 14 Oct 2019 19:33:52 +0000 (21:33 +0200)]
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 ...

5 years agobackport of WIP on \lambda\delta to matita 0.99.3
Ferruccio Guidi [Mon, 14 Oct 2019 10:07:33 +0000 (12:07 +0200)]
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

5 years agoupdate in ground_2 and basic_2
Ferruccio Guidi [Thu, 3 Oct 2019 15:14:08 +0000 (17:14 +0200)]
update in ground_2 and basic_2

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

5 years agoMerge remote-tracking branch 'origin/matita-lablgtk3'
Ferruccio Guidi [Tue, 1 Oct 2019 12:52:29 +0000 (14:52 +0200)]
Merge remote-tracking branch 'origin/matita-lablgtk3'

matita 0.99.4 now on master branch

5 years agoupdate in ground_2 and basic_2
Ferruccio Guidi [Mon, 30 Sep 2019 18:12:31 +0000 (20:12 +0200)]
update in ground_2 and basic_2

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

5 years agomatita gtk3: some bugs fixed matita-lablgtk3
Ferruccio Guidi [Sun, 29 Sep 2019 22:03:17 +0000 (00:03 +0200)]
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)

5 years agoMerge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita...
Ferruccio Guidi [Sun, 29 Sep 2019 20:43:50 +0000 (22:43 +0200)]
Merge branch 'matita-lablgtk3' of ssh://matita.cs.unibo.it:/srv/git/helm into matita-lablgtk3

5 years agoupdate in static_2
Ferruccio Guidi [Sun, 29 Sep 2019 18:54:08 +0000 (20:54 +0200)]
update in static_2

+ notation change for lifts and drops

5 years agoupdate in basic_2
Ferruccio Guidi [Sat, 28 Sep 2019 18:39:25 +0000 (20:39 +0200)]
update in basic_2

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

5 years agodebugging code removed
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 14:58:30 +0000 (16:58 +0200)]
debugging code removed

5 years agoMerge branch 'declarative' into matita-lablgtk3
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 14:52:38 +0000 (16:52 +0200)]
Merge branch 'declarative' into matita-lablgtk3

5 years agoChange Sort.merge (deprecated) with List.merge
Andrea Berlingieri [Fri, 27 Sep 2019 13:40:44 +0000 (15:40 +0200)]
Change Sort.merge (deprecated) with List.merge

5 years agoTest pretty printg of declarative tactics
Andrea Berlingieri [Thu, 26 Sep 2019 20:33:51 +0000 (22:33 +0200)]
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

5 years agoMake 'that is equivalent to' a standalone tactic
Andrea Berlingieri [Mon, 17 Jun 2019 08:10:31 +0000 (10:10 +0200)]
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.

5 years agoMany changes
Andrea Berlingieri [Sun, 19 May 2019 17:00:13 +0000 (19:00 +0200)]
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

5 years agoFix indentation
Andrea Berlingieri [Sun, 12 May 2019 15:32:43 +0000 (17:32 +0200)]
Fix indentation

5 years agoAdd support for proving cases in a different order
Andrea Berlingieri [Sun, 12 May 2019 15:19:18 +0000 (17:19 +0200)]
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

5 years agoAdd last declarative tactics, modify rewriting tactics
Andrea Berlingieri [Thu, 25 Apr 2019 13:07:24 +0000 (15:07 +0200)]
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

5 years agoChanges to declarative tactics, implementation of equality chain
Andrea Berlingieri [Tue, 23 Apr 2019 11:20:09 +0000 (13:20 +0200)]
Changes to declarative tactics, implementation of equality chain

Fix type for RewritingStep, add a type for Print Stack (a debug tool)

Fix PP for RewritingStep, generalized just_to_tactic_just for the type
[>`Auto of auto_params | `Term of NotationPt.term]

Add parsing rule for print_stack, fix parsing rules for obtain, conclude
e =

Fix indentation for declarative.ml

Change mk_just to return a tactic (instead of a lowtactic)

Modify extract_first_goal_from_status to take the first goal from the
stack, instead of the metasenv

Change assume, suppose, andelim and existselim to use distribute_tac

Add a mustdot function to check whether there's the need to call the
dot_tactic at the end. The dot tactic is used to focus on a single goal
at the time when there are multiple open goals

Change bydone to use the dot tactic to switch between multiple goals

Modify we_need_to_prove to use the dot_tac to focus on a single goal

Add a type_of_tactic_term function to extract the type of a tactic_term
(used in RewritingStep)

Implement rewritingstep, which covers conclude and =; obtain is in the
works

Implement print_stack, for debug purposes (prints the stack to stderr)

Modify declarative's signature to add the new functions

Add firs_tac to nTactic's signature

Change auto_lowtac's signature to return a tactic

Correct natural_deduction.ma for the new version. Had to change some
\forall with \Pi

5 years agoMany changes
Andrea Berlingieri [Sat, 13 Apr 2019 15:32:48 +0000 (17:32 +0200)]
Many changes

Change auto_params in grafiteAst.ml from being abstract on the 'term list
to being concretized to nterm list. Modify type just accordingly. Modify ntactic
types accordingly.

Add ExistsElim, AndElim, RewritingStep, Thesisbecomes types to ntactic.

Add pretty printing for ExistsElim, AndElim, RewritingStep, Thesisbecomes.

Add calls in grafite engine for the implementation of ExistsElim, AndElim, Thesisbecomes.

Add parsing rule for the "let x := t" tactic. It uses the NLetIn
ntactic.

Add parsing rules for Thesisbecomes and Rewritingstep (conclude, obtain
and =).

Modify mk_just to use the new auto_lowtac entry point for automation for
LCF-like tactics.

Remove same_type function in declarative.ml.

Add are_convertible function in declarative that uses beta-conversion.

Add a lambda_abstract tactic that abstracts the common parts of suppose
and assume. Add 3 Exception types for this tactic to handle error
situations. Modify assume and suppose accordingly

Add assert_tac that verifies that a given term is the same as the
conclusion and that two given types are beta-convertible, if a second
type is given. If all checks pass a continuation is exec'd, otherwise an
exception is raised.

Modify we_need_to_prove, by_just_we_proved to use assert_tac.

Add implementation of thesisbecomes.

Add implementation of existselim and andelim.

Modify declarative signature to add the new tactics.

Add a flag to index_local_equations and index_local_equations2 to
inhibit the use of global candidates. Modify all the functions that call
these two functions and the calls to those functions accordingly
(auto_main, do_something, top_cache, intros, auto_clusters)

Add a flag to auto_tac' to specify whether to use local candidates or
not. Modify the part where the local cands are calculated to check the
flag before proceeding.

Add auto_params to nnAuto.

Modify auto_tac to auto_tac' which takes the candidates to use
explicitly as a parameter and two flags that indicate whether to use
local candidates and whether to use only the given candidates.

Add a candidates_from_ctx function to calculate the candidates in a
given context.

Add a auto_lowtac entry point for LCF-like tactics.

Modify nnAuto signature to use auto_params instead of its explicit
version (nterm list * (string * string) list).

Add new "keywords" to matita.lang.

Add debug prints for a bug where the program would freeze. (They can
probably be removed)

5 years agoAdd drafts for some tactics
Andrea Berlingieri [Sun, 31 Mar 2019 12:58:51 +0000 (14:58 +0200)]
Add drafts for some tactics

Add drafts for assume, suppose, we_need_to_prove.

Add a just type to handle justfications in tactics.

Add drafts for the by_done and by_just_we_proved tactics.

Everything needs testing

5 years agoPartially restore the suppose tactic
Andrea Berlingieri [Thu, 14 Mar 2019 09:31:01 +0000 (10:31 +0100)]
Partially restore the suppose tactic

Add a type for the suppose tactic in GrafiteAst

Add pretty printing code for the suppose tactic

Add a parsing rule for the suppose tactic in GrafiteParser

Add a call in to the suppose tactic in GrafiteEngine

Add code for the suppose tactic in Declarative

Add syntax highlight tag for the suppose tactic

5 years agoPartially restore the assume tactic
Andrea Berlingieri [Wed, 13 Mar 2019 22:18:13 +0000 (23:18 +0100)]
Partially restore the assume tactic

Add a type for the assume tactic in GrafiteAst

Add pretty printing code for the assume tactic

Add a parsing rule for the assume tactic in GrafiteParser

Add a call in to the assume tactic in GrafiteEngine

Add a file for the declarative tactics to the ng_tactics module

Add code for the assume tactic in Declarative

Add syntax highlight tag for the assume tactic

Add the exact_tac signature to the interface file of nTactics

5 years agoporting to recent ocaml
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:55:14 +0000 (15:55 +0200)]
porting to recent ocaml

5 years ago...
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:54:23 +0000 (15:54 +0200)]
...

5 years agolablgtk3.sourceview3 => lablgtk3-sourceview3
Claudio Sacerdoti Coen [Fri, 27 Sep 2019 13:51:52 +0000 (15:51 +0200)]
lablgtk3.sourceview3 => lablgtk3-sourceview3

5 years agopatches for compilation with ocaml 4.0.5
Ferruccio Guidi [Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)]
patches for compilation with ocaml 4.0.5

+ lambdadelta website update

5 years agofinite_lambda restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:31:45 +0000 (16:31 +0100)]
finite_lambda restored

5 years agoreverse_complexity lib restored
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 15:25:21 +0000 (16:25 +0100)]
reverse_complexity lib restored

the toolkit.ma file contains errors. I have
commented out a few places

5 years agomake depend.opt
Claudio Sacerdoti Coen [Fri, 28 Dec 2018 14:33:07 +0000 (15:33 +0100)]
make depend.opt

5 years agomake dist repaired
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 13:02:54 +0000 (14:02 +0100)]
make dist repaired

- svn export => git archive

5 years agoversion upgrade
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 12:52:04 +0000 (13:52 +0100)]
version upgrade

5 years agoadded missing libs detection
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:25:46 +0000 (01:25 +0100)]
added missing libs detection

5 years agoMost warnings turned into errors and avoided
Claudio Sacerdoti Coen [Thu, 27 Dec 2018 00:19:15 +0000 (01:19 +0100)]
Most warnings turned into errors and avoided

5 years ago0.99.3 -> 0.99.4
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:17:21 +0000 (22:17 +0100)]
0.99.3 -> 0.99.4

5 years agoreport_error dialog ported to gtk3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 21:01:16 +0000 (22:01 +0100)]
report_error dialog ported to gtk3

5 years agoQuit without saving dialog fixed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 20:46:50 +0000 (21:46 +0100)]
Quit without saving dialog fixed

Ported to gtk3

5 years agouseful comment
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:40:44 +0000 (19:40 +0100)]
useful comment

5 years agoautomatically inserted aliases
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:20:21 +0000 (19:20 +0100)]
automatically inserted aliases

5 years agoMatita 0.99.* bug fixed: new alias insertion
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 18:18:24 +0000 (19:18 +0100)]
Matita 0.99.* bug fixed: new alias insertion

Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.

5 years agouse #run for dialog
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 16:03:07 +0000 (17:03 +0100)]
use #run for dialog

5 years agoLet the widget expand in the old way
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:38:07 +0000 (16:38 +0100)]
Let the widget expand in the old way

5 years agoOld glade2 file removed
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:11:24 +0000 (16:11 +0100)]
Old glade2 file removed

5 years agoBroken libs moved to broken_lib
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 15:09:34 +0000 (16:09 +0100)]
Broken libs moved to broken_lib

Some can probably be restored with some love.

5 years agolablgladecc => lablgladecc3
Claudio Sacerdoti Coen [Wed, 26 Dec 2018 12:38:12 +0000 (13:38 +0100)]
lablgladecc => lablgladecc3

It now compiles with lablgtk3 opam package

5 years agodisambiguationErrors now uses #run
Claudio Sacerdoti Coen [Mon, 24 Dec 2018 00:05:41 +0000 (01:05 +0100)]
disambiguationErrors now uses #run

correct Gtk behavior