]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoSetoids are now more pervasive.
Claudio Sacerdoti Coen [Wed, 3 Sep 2008 16:22:22 +0000 (16:22 +0000)]
Setoids are now more pervasive.

16 years agoUri ending in '' were not accepted. Fixed.
Claudio Sacerdoti Coen [Tue, 2 Sep 2008 13:59:47 +0000 (13:59 +0000)]
Uri ending in '' were not accepted. Fixed.

16 years agonew debugging option
Claudio Sacerdoti Coen [Mon, 1 Sep 2008 14:40:30 +0000 (14:40 +0000)]
new debugging option

16 years agoRelations are now closer to Sambin's ones. I.e. they range over Types
Claudio Sacerdoti Coen [Sun, 31 Aug 2008 23:43:25 +0000 (23:43 +0000)]
Relations are now closer to Sambin's ones. I.e. they range over Types
and not (sub)sets.

16 years ago...
Enrico Tassi [Thu, 28 Aug 2008 14:10:30 +0000 (14:10 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 28 Aug 2008 14:06:02 +0000 (14:06 +0000)]
...

16 years agonew baseuri for procedural CoRN
Ferruccio Guidi [Thu, 28 Aug 2008 10:47:30 +0000 (10:47 +0000)]
new baseuri for procedural CoRN
to follow the discharge name convention adopted in applyTransformation

16 years agoapplyTransformation: variable discharging in procedural/declarative script
Ferruccio Guidi [Thu, 28 Aug 2008 10:40:11 +0000 (10:40 +0000)]
applyTransformation: variable discharging in procedural/declarative script
                     reconstruction is now activated
we rebuilt the dependence files

16 years agocicDischarge: new module for discharging the explicit variables occurring in a
Ferruccio Guidi [Thu, 28 Aug 2008 10:33:25 +0000 (10:33 +0000)]
cicDischarge: new module for discharging the explicit variables occurring in a
              CiC object. This is used in the procedural/declarative
      reconstruction of Coq's library (es Coq/CoRN devels)
cicUniv: we add a default_ugraph set for now to oblivio_ugraph
acic_procedural: improved error handling
depend, depend.opt: we updated some

16 years agoConvergence is now defined.
Claudio Sacerdoti Coen [Wed, 27 Aug 2008 14:45:44 +0000 (14:45 +0000)]
Convergence is now defined.

16 years agoBetter notation, in particular for subset comprehension.
Claudio Sacerdoti Coen [Wed, 27 Aug 2008 09:37:21 +0000 (09:37 +0000)]
Better notation, in particular for subset comprehension.

16 years agoNotation |.| moved to core_notation.
Claudio Sacerdoti Coen [Tue, 26 Aug 2008 17:03:41 +0000 (17:03 +0000)]
Notation |.| moved to core_notation.

16 years agofixed some stuff
Enrico Tassi [Tue, 26 Aug 2008 14:56:18 +0000 (14:56 +0000)]
fixed some stuff

16 years agobug fix in inline syntax
Ferruccio Guidi [Mon, 25 Aug 2008 18:19:49 +0000 (18:19 +0000)]
bug fix in inline syntax

16 years ago...
Claudio Sacerdoti Coen [Mon, 25 Aug 2008 13:18:04 +0000 (13:18 +0000)]
...

16 years agoNew categories REL and BP.
Claudio Sacerdoti Coen [Mon, 25 Aug 2008 13:17:48 +0000 (13:17 +0000)]
New categories REL and BP.
Nice naive infrastructure for setoid rewriting.

16 years agoNew cool "type-checking" notation using colors and non-linear patterns.
Claudio Sacerdoti Coen [Mon, 25 Aug 2008 13:16:53 +0000 (13:16 +0000)]
New cool "type-checking" notation using colors and non-linear patterns.
Still not working propertly for and and for-all elimination.

16 years agoDo not mess with my window manager: the Cic Browsers are no longer slaves to
Claudio Sacerdoti Coen [Mon, 25 Aug 2008 13:15:54 +0000 (13:15 +0000)]
Do not mess with my window manager: the Cic Browsers are no longer slaves to
the main window.

16 years agoNon-linear patterns are now allowed in notations.
Claudio Sacerdoti Coen [Mon, 25 Aug 2008 13:14:54 +0000 (13:14 +0000)]
Non-linear patterns are now allowed in notations.

16 years agotranscript: bug fix in the generation of axioms
Ferruccio Guidi [Mon, 25 Aug 2008 10:27:03 +0000 (10:27 +0000)]
transcript: bug fix in the generation of axioms
            variables are now unexported
CoRN-Procedural: regenerated and Makefile improved

16 years ago...
Enrico Tassi [Sun, 24 Aug 2008 15:05:32 +0000 (15:05 +0000)]
...

16 years agoProcedural: bug fix in comment generation
Ferruccio Guidi [Sat, 23 Aug 2008 19:38:53 +0000 (19:38 +0000)]
Procedural: bug fix in comment generation
applyTransformation: now mma compilation fails on procedural generation errors
matitacLib: when the mma fails the generated ma is removed

16 years ago...
Enrico Tassi [Sat, 23 Aug 2008 19:17:50 +0000 (19:17 +0000)]
...

16 years ago...
Enrico Tassi [Sat, 23 Aug 2008 19:17:31 +0000 (19:17 +0000)]
...

16 years agoDefinition of categories.
Claudio Sacerdoti Coen [Sat, 23 Aug 2008 19:14:54 +0000 (19:14 +0000)]
Definition of categories.
Proof that basic pairs form a category.

16 years agoSome notation moved to core_notation.
Claudio Sacerdoti Coen [Sat, 23 Aug 2008 19:12:21 +0000 (19:12 +0000)]
Some notation moved to core_notation.
A few new things in datatypes/subsets and related stuff.

16 years agoAlso create the graphviz graph.
Claudio Sacerdoti Coen [Sat, 23 Aug 2008 19:11:15 +0000 (19:11 +0000)]
Also create the graphviz graph.

16 years agoNew debug item to print aliases.
Claudio Sacerdoti Coen [Sat, 23 Aug 2008 19:10:31 +0000 (19:10 +0000)]
New debug item to print aliases.

16 years agoProcedural: explicit flavour specification for constants is now working
Ferruccio Guidi [Sat, 23 Aug 2008 13:18:57 +0000 (13:18 +0000)]
Procedural: explicit flavour specification for constants is now working
            procedural inlining of inductive types is now working
    fixup in the generation of comments
grafiteAstPp: syntax fixup
transcript: now generates explicit flavour for inlined constants
            so we distinguish between definitions and theorems :)
    [the attributes are not present when we inline from Coq's library]
CoRN-Procedural: mma files regenerated with explicit flavours

16 years agonotation with mstyle attributes, like colors and size
Enrico Tassi [Sat, 23 Aug 2008 04:11:04 +0000 (04:11 +0000)]
notation with mstyle attributes, like colors and size

16 years ago...
Enrico Tassi [Sat, 23 Aug 2008 04:08:58 +0000 (04:08 +0000)]
...

16 years agopango escape fixed
Enrico Tassi [Thu, 21 Aug 2008 23:08:44 +0000 (23:08 +0000)]
pango escape fixed

16 years ago...
Enrico Tassi [Thu, 21 Aug 2008 22:47:43 +0000 (22:47 +0000)]
...

16 years agoAvoid warning.
Claudio Sacerdoti Coen [Thu, 21 Aug 2008 17:36:35 +0000 (17:36 +0000)]
Avoid warning.

16 years agoAdded catching of an exception to implement a missing occur check:
Claudio Sacerdoti Coen [Thu, 21 Aug 2008 17:35:19 +0000 (17:35 +0000)]
Added catching of an exception to implement a missing occur check:
when unifying ?1 : T with t : T', T and T' are unified first. If ?1
occurs in T', it is moved from the metasenv to the subst, and the
exception here used to escape.

16 years agosvn:ignore property is now swr correctly`
Ferruccio Guidi [Thu, 21 Aug 2008 10:43:03 +0000 (10:43 +0000)]
svn:ignore property is now swr correctly`

16 years agobasic support for imposed flavour in procedural object rendering
Ferruccio Guidi [Thu, 21 Aug 2008 10:31:16 +0000 (10:31 +0000)]
basic support for imposed flavour in procedural object rendering

16 years agoescape < in pango attrs
Enrico Tassi [Sun, 17 Aug 2008 14:38:40 +0000 (14:38 +0000)]
escape < in pango attrs

16 years agoadded support for font scaling to autogui
Enrico Tassi [Sat, 16 Aug 2008 07:27:52 +0000 (07:27 +0000)]
added support for font scaling to autogui

16 years agoadded interpretation for \naturals, \rationals, and \integers
Enrico Tassi [Sat, 16 Aug 2008 07:14:26 +0000 (07:14 +0000)]
added interpretation for \naturals, \rationals, and \integers

16 years agoFixed two legacy comments
Wilmer Ricciotti [Tue, 12 Aug 2008 21:11:17 +0000 (21:11 +0000)]
Fixed two legacy comments

16 years agofixed recursiveness check
Enrico Tassi [Fri, 1 Aug 2008 07:34:13 +0000 (07:34 +0000)]
fixed recursiveness check

16 years agofixed recursiveness check
Enrico Tassi [Fri, 1 Aug 2008 07:29:58 +0000 (07:29 +0000)]
fixed recursiveness check

16 years agofixed check, if 0 constructors then no List.nth is allowed
Enrico Tassi [Wed, 30 Jul 2008 22:41:05 +0000 (22:41 +0000)]
fixed check, if 0 constructors then no List.nth is allowed

16 years agoallowed sort elim now check for recursive types
Enrico Tassi [Wed, 30 Jul 2008 15:19:04 +0000 (15:19 +0000)]
allowed sort elim now check for recursive types

16 years agofixed allowed sort elim
Enrico Tassi [Wed, 30 Jul 2008 15:08:17 +0000 (15:08 +0000)]
fixed allowed sort elim

16 years agoMissing check implemented: uniformity of left parameters in contravariant
Claudio Sacerdoti Coen [Wed, 30 Jul 2008 11:14:33 +0000 (11:14 +0000)]
Missing check implemented: uniformity of left parameters in contravariant
position was missing from strictly_positive.

16 years agoMissing check in positivity implemented: we did not check uniformity for
Claudio Sacerdoti Coen [Wed, 30 Jul 2008 09:00:35 +0000 (09:00 +0000)]
Missing check in positivity implemented: we did not check uniformity for
left parameters in contravariant position.

16 years ago- too strict check on left parameters of constructors in guarded by constructors...
Enrico Tassi [Fri, 25 Jul 2008 17:01:49 +0000 (17:01 +0000)]
- too strict check on left parameters of constructors in guarded by constructors removed
- the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the
  new kernel since:
    o  recursive/corecursive objects are now closed terms
    o  we do not allow (yet?) to pass co-recursive functions around
    o  we do check that the arguments of the application of a fix/cofix do not
       contain the function we are checking for GBC

16 years agoAST to ASTFE completed up to a few computational (!!!) axioms.
Claudio Sacerdoti Coen [Fri, 25 Jul 2008 15:09:36 +0000 (15:09 +0000)]
AST to ASTFE completed up to a few computational (!!!) axioms.

16 years ago...
Enrico Tassi [Wed, 23 Jul 2008 21:50:35 +0000 (21:50 +0000)]
...

16 years ago0.5.3
Enrico Tassi [Wed, 23 Jul 2008 21:48:36 +0000 (21:48 +0000)]
0.5.3

16 years ago0.5.3
Enrico Tassi [Wed, 23 Jul 2008 21:30:49 +0000 (21:30 +0000)]
0.5.3

16 years agosome more fixes
Enrico Tassi [Wed, 23 Jul 2008 21:09:56 +0000 (21:09 +0000)]
some more fixes

16 years agofixed some GUI glitches
Enrico Tassi [Wed, 23 Jul 2008 21:05:06 +0000 (21:05 +0000)]
fixed some GUI glitches

16 years agopositivity check fixed
Enrico Tassi [Wed, 23 Jul 2008 16:29:35 +0000 (16:29 +0000)]
positivity check fixed

16 years ago...
Enrico Tassi [Wed, 23 Jul 2008 16:12:36 +0000 (16:12 +0000)]
...

16 years agopositivity check fixed, some subterms were erroneously skipped
Enrico Tassi [Wed, 23 Jul 2008 16:09:17 +0000 (16:09 +0000)]
positivity check fixed, some subterms were erroneously skipped

16 years agouniverses in CicBrowser
Enrico Tassi [Wed, 23 Jul 2008 11:43:26 +0000 (11:43 +0000)]
universes in CicBrowser

16 years agobetter ranking interface
Enrico Tassi [Wed, 23 Jul 2008 11:41:37 +0000 (11:41 +0000)]
better ranking interface

16 years agobetter tex/utf8 win
Enrico Tassi [Wed, 23 Jul 2008 10:54:28 +0000 (10:54 +0000)]
better tex/utf8 win

16 years agobetter cb
Enrico Tassi [Wed, 23 Jul 2008 10:51:55 +0000 (10:51 +0000)]
better cb

16 years agobetter UI for TeX/Unicode and terms grammar
Enrico Tassi [Wed, 23 Jul 2008 10:47:19 +0000 (10:47 +0000)]
better UI for TeX/Unicode and terms grammar

16 years agoUpdate.
Claudio Sacerdoti Coen [Wed, 23 Jul 2008 09:53:56 +0000 (09:53 +0000)]
Update.

16 years agoremove bad aliases from toolbox
Enrico Tassi [Wed, 23 Jul 2008 09:02:20 +0000 (09:02 +0000)]
remove bad aliases from toolbox

16 years agoUniverse levels fixed.
Claudio Sacerdoti Coen [Wed, 23 Jul 2008 08:20:09 +0000 (08:20 +0000)]
Universe levels fixed.

16 years agomatitadep: we now handle the inline of an uri, we removed the -exclude option
Ferruccio Guidi [Tue, 22 Jul 2008 17:28:07 +0000 (17:28 +0000)]
matitadep: we now handle the inline of an uri, we removed the -exclude option
matitaInit: we removed the -drop option (now handled automatically)
transcript: we removed the baseuri generation
CoRN-Procedural: the mma files and the depends file are now available

16 years agotranscript: now we can generate procedural output
Ferruccio Guidi [Tue, 22 Jul 2008 12:43:10 +0000 (12:43 +0000)]
transcript: now we can generate procedural output
CoRN-Procedural: development started:
                 we aim at the procedural reconstruction of CoRN

16 years ago...
Enrico Tassi [Tue, 22 Jul 2008 11:52:25 +0000 (11:52 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 22 Jul 2008 08:34:00 +0000 (08:34 +0000)]
...

16 years agoIn some universe, membership is a morphism.
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 08:00:09 +0000 (08:00 +0000)]
In some universe, membership is a morphism.

16 years agoSambin's & Valentini's toolbox (???)
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 07:01:46 +0000 (07:01 +0000)]
Sambin's & Valentini's toolbox (???)

16 years agoDependencies removed.
Claudio Sacerdoti Coen [Tue, 22 Jul 2008 07:01:06 +0000 (07:01 +0000)]
Dependencies removed.

16 years ago...
Enrico Tassi [Mon, 21 Jul 2008 19:26:28 +0000 (19:26 +0000)]
...

16 years agofrac is an infix operator!
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:42 +0000 (19:05 +0000)]
frac is an infix operator!

16 years agoError message improved.
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:27 +0000 (19:05 +0000)]
Error message improved.

16 years agoRendering of \infrule improved.
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 19:05:12 +0000 (19:05 +0000)]
Rendering of \infrule improved.

16 years agowe implemented the support for generating ma files from mma files
Ferruccio Guidi [Mon, 21 Jul 2008 18:10:30 +0000 (18:10 +0000)]
we implemented the support for generating ma files from mma files

16 years agoadded notes about notation
Enrico Tassi [Mon, 21 Jul 2008 13:38:38 +0000 (13:38 +0000)]
added notes about notation

16 years agoadd conf key matita.debug_menu
Enrico Tassi [Mon, 21 Jul 2008 11:47:15 +0000 (11:47 +0000)]
add conf key matita.debug_menu

16 years agoavoid empty hvbox
Enrico Tassi [Mon, 21 Jul 2008 11:34:35 +0000 (11:34 +0000)]
avoid empty hvbox

16 years ago...
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 10:55:23 +0000 (10:55 +0000)]
...

16 years agoSemantic analysis implemented (sort of).
Claudio Sacerdoti Coen [Mon, 21 Jul 2008 10:11:49 +0000 (10:11 +0000)]
Semantic analysis implemented (sort of).

16 years ago...
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 15:11:22 +0000 (15:11 +0000)]
...

16 years agoNew input notation for bottom-up tree construction finished.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 14:47:29 +0000 (14:47 +0000)]
New input notation for bottom-up tree construction finished.

16 years agoSnapshot.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 14:23:01 +0000 (14:23 +0000)]
Snapshot.

16 years agoInput notation.
Claudio Sacerdoti Coen [Fri, 18 Jul 2008 13:13:43 +0000 (13:13 +0000)]
Input notation.

16 years agobetter metavariable context
Enrico Tassi [Fri, 18 Jul 2008 12:55:24 +0000 (12:55 +0000)]
better metavariable context

16 years agometavariable context has a separator now
Enrico Tassi [Fri, 18 Jul 2008 12:51:05 +0000 (12:51 +0000)]
metavariable context has a separator now

16 years agoexception inside regex callback not re-raised if equal to sys.break
Enrico Tassi [Fri, 18 Jul 2008 08:30:09 +0000 (08:30 +0000)]
exception inside regex callback not re-raised if equal to sys.break

16 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 13:28:34 +0000 (13:28 +0000)]
Bugs fixed:
\frac is an infix operator
\infrule is a prefix operator

16 years ago1 => \\e
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 13:27:14 +0000 (13:27 +0000)]
1 => \\e

16 years agoExecutables are now ignored.
Claudio Sacerdoti Coen [Thu, 17 Jul 2008 12:02:22 +0000 (12:02 +0000)]
Executables are now ignored.

16 years agoProcedural: some comments added in the generated script
Ferruccio Guidi [Wed, 16 Jul 2008 18:16:19 +0000 (18:16 +0000)]
Procedural: some comments added in the generated script
tests/fguidi.ma: we removed the dependence from legacy/coq.ma
ApplyTransformation: new function procedural_text_of_cic_term
                     for use in matitaScript (still disabled)

16 years agonotations for lists adds some breaking points
Enrico Tassi [Wed, 16 Jul 2008 16:16:30 +0000 (16:16 +0000)]
notations for lists adds some breaking points

16 years agoDuplicated doc removed.
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 14:02:07 +0000 (14:02 +0000)]
Duplicated doc removed.

16 years agoSnapshot (not working).
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 13:58:11 +0000 (13:58 +0000)]
Snapshot (not working).

16 years agoa) update with upstream version
Claudio Sacerdoti Coen [Wed, 16 Jul 2008 12:37:24 +0000 (12:37 +0000)]
a) update with upstream version
b) new: implemented semantic analyzer from untyped to typed AST for
   an imperative structured function-less C compiler
c) all URIs removed from .ma files

16 years agocic2acic: new function acic_term_of_cic_term
Ferruccio Guidi [Tue, 15 Jul 2008 17:54:23 +0000 (17:54 +0000)]
cic2acic: new function acic_term_of_cic_term
matita/Makefile: LAMBDA-TYPES tested only in opt mode

16 years agomore notation moved to core notation, unification of duplicated CProp connectives
Enrico Tassi [Tue, 15 Jul 2008 17:01:14 +0000 (17:01 +0000)]
more notation moved to core notation, unification of duplicated CProp connectives