]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

16 years agoSince CProp_i = Type_i everything lowered without 2 distinct Sigma.
Enrico Tassi [Tue, 15 Jul 2008 12:01:23 +0000 (12:01 +0000)]
Since CProp_i = Type_i everything lowered without 2 distinct Sigma.

16 years agoCProp_i <= Type_i , Type_i <= CProp_i
Enrico Tassi [Tue, 15 Jul 2008 12:00:24 +0000 (12:00 +0000)]
CProp_i <= Type_i , Type_i <= CProp_i

16 years agomodels over N fixed
Enrico Tassi [Tue, 15 Jul 2008 10:16:06 +0000 (10:16 +0000)]
models over N fixed

16 years agonew q_function representation
Enrico Tassi [Tue, 15 Jul 2008 09:18:23 +0000 (09:18 +0000)]
new q_function representation

16 years agoremoved dummy comment
Enrico Tassi [Tue, 15 Jul 2008 09:09:30 +0000 (09:09 +0000)]
removed dummy comment

16 years agoUsing Prop conjuction on Props lowers the universes.
Enrico Tassi [Tue, 15 Jul 2008 09:08:15 +0000 (09:08 +0000)]
Using Prop conjuction on Props lowers the universes.
SigT instead of ExT

16 years agolambda-delta: we added the support for position indexes in global references
Ferruccio Guidi [Mon, 14 Jul 2008 20:17:22 +0000 (20:17 +0000)]
lambda-delta: we added the support for position indexes in global references
              we added a pretty printer for the intermediate language
librarian   : utime stamps now appear only in debug mode

16 years agoProcedural: we added the support for rendering definitions and axioms
Ferruccio Guidi [Mon, 14 Jul 2008 11:57:42 +0000 (11:57 +0000)]
Procedural: we added the support for rendering definitions and axioms

16 years agoProcedural: we added the support for theorem flavours and we fixed the handling ...
Ferruccio Guidi [Sun, 13 Jul 2008 15:02:49 +0000 (15:02 +0000)]
Procedural: we added the support for theorem flavours and we fixed the handling             of unexpected proof constructions

16 years agocicUtil : we added a context to is_sober to check for consistancy
Ferruccio Guidi [Sun, 13 Jul 2008 11:06:20 +0000 (11:06 +0000)]
cicUtil            : we added a context to is_sober to check for consistancy
                     of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
                     of the expected prod :)
acic2Procedural    : we added a consistancy check that was missing

16 years agoProcedural: bug fix in the procedural rendering of the abstraction
Ferruccio Guidi [Sat, 12 Jul 2008 22:17:46 +0000 (22:17 +0000)]
Procedural: bug fix in the procedural rendering of the abstraction

16 years agolibrarian: retrieval of buildable files speeded up a lot
Ferruccio Guidi [Sat, 12 Jul 2008 20:40:30 +0000 (20:40 +0000)]
librarian: retrieval of buildable files speeded up a lot
Procedural: some bug fixes
termContentPres.ml: syntax of let-in construction fixed
LAMBDA-TYPES: some improvements in the Makefile

16 years agoNew feature/bug fixed (hopefully): it is now possible to use fixed (term)
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:43:21 +0000 (11:43 +0000)]
New feature/bug fixed (hopefully): it is now possible to use fixed (term)
variables in fold bodies.
The notation for exists is now fully working as expected.

16 years agoNotation for existential partially fixed: it is now possible to write
Claudio Sacerdoti Coen [Sat, 12 Jul 2008 11:17:17 +0000 (11:17 +0000)]
Notation for existential partially fixed: it is now possible to write
\exists a,b,c:T.P
(possibly omitting the type).
In any case, however, the type is got rid of during parsing.

16 years agoA very nice experiment using notation: we define the notation for natural
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 17:22:19 +0000 (17:22 +0000)]
A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).

16 years agoExists is no longer an ad-hoc notation hard-coded in the parser.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 16:49:18 +0000 (16:49 +0000)]
Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.

16 years agoAdded new ternary layout \infrule premises conclusion name.
Claudio Sacerdoti Coen [Fri, 11 Jul 2008 14:29:09 +0000 (14:29 +0000)]
Added new ternary layout \infrule premises conclusion name.
Very useful to render proof terms as trees.

16 years agovalue has a specification
Enrico Tassi [Thu, 10 Jul 2008 10:16:48 +0000 (10:16 +0000)]
value has a specification

16 years agoupdated changelog
Enrico Tassi [Thu, 10 Jul 2008 08:13:16 +0000 (08:13 +0000)]
updated changelog

16 years agomore work on dama
Enrico Tassi [Thu, 10 Jul 2008 08:00:45 +0000 (08:00 +0000)]
more work on dama

16 years agofixed regression in casting an argument to funclass, this incidentally leaded to...
Enrico Tassi [Thu, 10 Jul 2008 08:00:30 +0000 (08:00 +0000)]
fixed regression in casting an argument to funclass, this incidentally leaded to a single look_for_coercion_function

16 years agosome bug fixes
Ferruccio Guidi [Wed, 9 Jul 2008 18:24:46 +0000 (18:24 +0000)]
some bug fixes