]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agonatural deduction support for lemmas with premises
Enrico Tassi [Sun, 30 Nov 2008 21:00:04 +0000 (21:00 +0000)]
natural deduction support for lemmas with premises

16 years agolambda-delta/toplevel: improved transformation from automath (20 secs gained)
Ferruccio Guidi [Sun, 30 Nov 2008 18:23:11 +0000 (18:23 +0000)]
lambda-delta/toplevel: improved transformation from automath (20 secs gained)
                       bug fix in the default arguments specification
       reverse indexes are now supported
transcript: unused parser productions removed

16 years agocicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :)
Ferruccio Guidi [Fri, 28 Nov 2008 21:41:19 +0000 (21:41 +0000)]
cicDischarge: final fixup. Now correctly processes Coq/Init/Logic.mma :)
              We handle missing abstractions in MutCase output type
procedural/Coq: we removed the depence from legacy

16 years agong_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed
Ferruccio Guidi [Fri, 28 Nov 2008 18:28:58 +0000 (18:28 +0000)]
ng_disambiguation ng_kernel ng_refiner disambiguation: svn:ignore fixed
hExtlib: the map of list_findopt takes the position in the list (starts at 0)
cicRefine, acic2astMatcher, grafiteEngine: updated accordingly
cicUtil cicDischarge: bug fixes
cicSubstitution: new function lift_map for non-linear relocation
proceduralOptimizer: initial support for contrlling critical optimizations

16 years agoit works!
Enrico Tassi [Fri, 28 Nov 2008 17:48:52 +0000 (17:48 +0000)]
it works!

16 years agonew disambiguator almost attached
Enrico Tassi [Fri, 28 Nov 2008 17:17:02 +0000 (17:17 +0000)]
new disambiguator almost attached

16 years ago\forall x:?. and \forall x. both generate a meta for a type
Enrico Tassi [Fri, 28 Nov 2008 16:18:11 +0000 (16:18 +0000)]
\forall x:?. and \forall x. both generate a meta for a type

16 years agometas for terms have height 3
Enrico Tassi [Fri, 28 Nov 2008 16:17:22 +0000 (16:17 +0000)]
metas for terms have height 3

16 years ago...
Enrico Tassi [Fri, 28 Nov 2008 12:18:09 +0000 (12:18 +0000)]
...

16 years ago...
Enrico Tassi [Fri, 28 Nov 2008 12:13:12 +0000 (12:13 +0000)]
...

16 years agovirtualbox guide almost ok
Enrico Tassi [Fri, 28 Nov 2008 12:11:25 +0000 (12:11 +0000)]
virtualbox guide almost ok

16 years ago...
Enrico Tassi [Fri, 28 Nov 2008 11:35:45 +0000 (11:35 +0000)]
...

16 years ago...
Enrico Tassi [Fri, 28 Nov 2008 11:33:39 +0000 (11:33 +0000)]
...

16 years ago...
Claudio Sacerdoti Coen [Thu, 27 Nov 2008 21:29:54 +0000 (21:29 +0000)]
...

16 years ago...
Claudio Sacerdoti Coen [Thu, 27 Nov 2008 21:29:23 +0000 (21:29 +0000)]
...

16 years ago...
Claudio Sacerdoti Coen [Thu, 27 Nov 2008 21:23:03 +0000 (21:23 +0000)]
...

16 years agoNew modules stack:
Enrico Tassi [Thu, 27 Nov 2008 17:44:31 +0000 (17:44 +0000)]
New modules stack:
grafiteDisambiguator | cicDisambiguator |
                                        | multiPassDisambiagutor |disambiguate
                       nCicDisambiguator|

16 years agocic_disambiguation splitted into disambiguation and cic_disambiguation
Enrico Tassi [Thu, 27 Nov 2008 12:39:24 +0000 (12:39 +0000)]
cic_disambiguation splitted into disambiguation and cic_disambiguation

16 years agodisambiguate.ml splitted into disambiguate.ml and cicDisambiguate.ml
Enrico Tassi [Thu, 27 Nov 2008 12:26:03 +0000 (12:26 +0000)]
disambiguate.ml splitted into disambiguate.ml and cicDisambiguate.ml

16 years ago1. grafiteDisambiguator => multiPassDisambiguator
Enrico Tassi [Thu, 27 Nov 2008 12:24:38 +0000 (12:24 +0000)]
1. grafiteDisambiguator => multiPassDisambiguator
2.

16 years agonew kernel is compiled since the META of grafite_parser depends on the META of ng_dis...
Enrico Tassi [Thu, 27 Nov 2008 10:34:26 +0000 (10:34 +0000)]
new kernel is compiled since the META of grafite_parser depends on the META of ng_disambiguation

16 years ago...
Enrico Tassi [Thu, 27 Nov 2008 10:32:18 +0000 (10:32 +0000)]
...

16 years agonotation now digests Cic.Cast, not sure the precedence level is handled correctly
Enrico Tassi [Thu, 27 Nov 2008 10:21:52 +0000 (10:21 +0000)]
notation now digests Cic.Cast, not sure the precedence level is handled correctly

16 years agodisambiguation should not fail if the new refiner fails
Enrico Tassi [Thu, 27 Nov 2008 09:37:43 +0000 (09:37 +0000)]
disambiguation should not fail if the new refiner fails

16 years ago...
Enrico Tassi [Wed, 26 Nov 2008 17:47:27 +0000 (17:47 +0000)]
...

16 years agoRe-added exception, just for now (debugging).
Enrico Tassi [Wed, 26 Nov 2008 17:24:36 +0000 (17:24 +0000)]
Re-added exception, just for now (debugging).

16 years agoalmost done
Enrico Tassi [Wed, 26 Nov 2008 17:11:00 +0000 (17:11 +0000)]
almost done

16 years agodisambiguation even more abstracted
Enrico Tassi [Wed, 26 Nov 2008 16:11:47 +0000 (16:11 +0000)]
disambiguation even more abstracted

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:30:33 +0000 (19:30 +0000)]
...

16 years agocicUtil: we moved here pp_term from proceduralHelpers
Ferruccio Guidi [Tue, 25 Nov 2008 19:27:41 +0000 (19:27 +0000)]
cicUtil: we moved here pp_term from proceduralHelpers
cicDischarge: some bugs fixed
transcript: we now support explicit declaration of dependences
procedural/Coq: we added an explicit dependence to Init/Prelude where needed

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:27:30 +0000 (19:27 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:21:52 +0000 (19:21 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:21:01 +0000 (19:21 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:15:53 +0000 (19:15 +0000)]
...

16 years ago...
Enrico Tassi [Tue, 25 Nov 2008 19:13:52 +0000 (19:13 +0000)]
...

16 years agomore on the livecd in the manual
Enrico Tassi [Tue, 25 Nov 2008 19:10:15 +0000 (19:10 +0000)]
more on the livecd in the manual

16 years ago....
Enrico Tassi [Mon, 24 Nov 2008 18:11:08 +0000 (18:11 +0000)]
....

16 years ago...
Enrico Tassi [Mon, 24 Nov 2008 17:27:41 +0000 (17:27 +0000)]
...

16 years agoformal topologies
Enrico Tassi [Mon, 24 Nov 2008 16:19:54 +0000 (16:19 +0000)]
formal topologies

16 years agofix some non tex symbols
Enrico Tassi [Mon, 24 Nov 2008 10:45:13 +0000 (10:45 +0000)]
fix some non tex symbols

16 years agosymbolic links to use the uri manager from ng_kernel
Ferruccio Guidi [Sat, 22 Nov 2008 21:19:30 +0000 (21:19 +0000)]
symbolic links to use the uri manager from ng_kernel

16 years agoprint an error message if graphviz is not found
Enrico Tassi [Sat, 22 Nov 2008 16:53:58 +0000 (16:53 +0000)]
print an error message if graphviz is not found

16 years agoif gnome-help is not installed, prints an error message
Enrico Tassi [Sat, 22 Nov 2008 16:48:15 +0000 (16:48 +0000)]
if gnome-help is not installed, prints an error message

16 years agobetter manual generation
Enrico Tassi [Sat, 22 Nov 2008 14:01:14 +0000 (14:01 +0000)]
better manual generation

16 years ago...
Enrico Tassi [Fri, 21 Nov 2008 17:58:08 +0000 (17:58 +0000)]
...

16 years agoone more lazy/loc
Enrico Tassi [Fri, 21 Nov 2008 16:25:55 +0000 (16:25 +0000)]
one more lazy/loc

16 years agoaccording to camlp5 sources, the dummy loc should be 0,0 and not -1,-1
Enrico Tassi [Fri, 21 Nov 2008 16:16:52 +0000 (16:16 +0000)]
according to camlp5 sources, the dummy loc should be 0,0 and not -1,-1

16 years agoloc * lazy string -> (loc * string) lazy
Enrico Tassi [Fri, 21 Nov 2008 16:00:06 +0000 (16:00 +0000)]
loc * lazy string -> (loc * string) lazy

16 years agodisambiguation now returns and takes in input the substitution
Enrico Tassi [Fri, 21 Nov 2008 15:15:43 +0000 (15:15 +0000)]
disambiguation now returns and takes in input the substitution

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 18:13:50 +0000 (18:13 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 18:13:18 +0000 (18:13 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 16:06:24 +0000 (16:06 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 16:04:25 +0000 (16:04 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 16:02:44 +0000 (16:02 +0000)]
...

16 years agodama almost ok
Enrico Tassi [Thu, 20 Nov 2008 16:00:06 +0000 (16:00 +0000)]
dama almost ok

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 15:55:08 +0000 (15:55 +0000)]
...

16 years ago...
Enrico Tassi [Thu, 20 Nov 2008 15:54:36 +0000 (15:54 +0000)]
...

16 years agoreverted
Enrico Tassi [Thu, 20 Nov 2008 15:54:16 +0000 (15:54 +0000)]
reverted

16 years agodama into the library
Enrico Tassi [Thu, 20 Nov 2008 15:53:09 +0000 (15:53 +0000)]
dama into the library

16 years agox2sx declared as coercion and used when possible
Enrico Tassi [Wed, 19 Nov 2008 18:38:27 +0000 (18:38 +0000)]
x2sx declared as coercion and used when possible

16 years agorenaming
Enrico Tassi [Wed, 19 Nov 2008 12:19:26 +0000 (12:19 +0000)]
renaming

16 years ago...
Enrico Tassi [Wed, 19 Nov 2008 12:13:44 +0000 (12:13 +0000)]
...

16 years ago0.5.5
Enrico Tassi [Tue, 18 Nov 2008 12:50:57 +0000 (12:50 +0000)]
0.5.5

16 years ago...
Enrico Tassi [Mon, 17 Nov 2008 19:46:56 +0000 (19:46 +0000)]
...

16 years ago...
Enrico Tassi [Mon, 17 Nov 2008 16:20:36 +0000 (16:20 +0000)]
...

16 years agoexercises ready
Enrico Tassi [Mon, 17 Nov 2008 16:20:08 +0000 (16:20 +0000)]
exercises ready

16 years agoall ex done
Enrico Tassi [Mon, 17 Nov 2008 11:44:55 +0000 (11:44 +0000)]
all ex done

16 years ago...
Enrico Tassi [Sun, 16 Nov 2008 10:33:10 +0000 (10:33 +0000)]
...

16 years ago....
Enrico Tassi [Sun, 16 Nov 2008 10:31:08 +0000 (10:31 +0000)]
....

16 years agofixed
Enrico Tassi [Sun, 16 Nov 2008 10:30:30 +0000 (10:30 +0000)]
fixed

16 years agoremoved some printings
Enrico Tassi [Sun, 16 Nov 2008 10:08:58 +0000 (10:08 +0000)]
removed some printings

16 years agocommented out unfinished proof
Enrico Tassi [Sun, 16 Nov 2008 10:05:17 +0000 (10:05 +0000)]
commented out unfinished proof

16 years agoremoved some printings
Enrico Tassi [Sun, 16 Nov 2008 10:03:48 +0000 (10:03 +0000)]
removed some printings

16 years agobetter spacing
Enrico Tassi [Sat, 15 Nov 2008 17:48:16 +0000 (17:48 +0000)]
better spacing

16 years agoapply rule (lem EM) works
Enrico Tassi [Sat, 15 Nov 2008 17:26:07 +0000 (17:26 +0000)]
apply rule (lem EM) works

16 years agomissing subst added, now apply rule is probably enough to replace apply
Enrico Tassi [Sat, 15 Nov 2008 17:25:41 +0000 (17:25 +0000)]
missing subst added, now apply rule is probably enough to replace apply

16 years agoNew bug.
Claudio Sacerdoti Coen [Sat, 15 Nov 2008 15:45:52 +0000 (15:45 +0000)]
New bug.

16 years agono more prove in palette
Enrico Tassi [Sat, 15 Nov 2008 15:32:59 +0000 (15:32 +0000)]
no more prove in palette

16 years agofixed or-in-left
Enrico Tassi [Sat, 15 Nov 2008 15:27:22 +0000 (15:27 +0000)]
fixed or-in-left

16 years agofixed not-e
Enrico Tassi [Sat, 15 Nov 2008 15:20:33 +0000 (15:20 +0000)]
fixed not-e

16 years agoAnother bug.
Claudio Sacerdoti Coen [Sat, 15 Nov 2008 15:15:46 +0000 (15:15 +0000)]
Another bug.

16 years agoThis commit shows a bug.
Claudio Sacerdoti Coen [Sat, 15 Nov 2008 15:13:38 +0000 (15:13 +0000)]
This commit shows a bug.

16 years agoalmost ready
Enrico Tassi [Sat, 15 Nov 2008 14:56:05 +0000 (14:56 +0000)]
almost ready

16 years agorules fixed
Enrico Tassi [Sat, 15 Nov 2008 14:33:49 +0000 (14:33 +0000)]
rules fixed

16 years agomake all/clean implemented
Enrico Tassi [Sat, 15 Nov 2008 13:21:48 +0000 (13:21 +0000)]
make all/clean implemented

16 years agohousekeeping
Enrico Tassi [Sat, 15 Nov 2008 13:18:05 +0000 (13:18 +0000)]
housekeeping

16 years agohousekeeping
Enrico Tassi [Sat, 15 Nov 2008 13:17:00 +0000 (13:17 +0000)]
housekeeping

16 years agohouse keeping
Enrico Tassi [Sat, 15 Nov 2008 13:14:48 +0000 (13:14 +0000)]
house keeping

16 years agodisambiguation can use a goal as hint for the expected type
Enrico Tassi [Sat, 15 Nov 2008 12:53:35 +0000 (12:53 +0000)]
disambiguation can use a goal as hint for the expected type

16 years agonatural deduction palette
Enrico Tassi [Sat, 15 Nov 2008 12:52:22 +0000 (12:52 +0000)]
natural deduction palette

16 years agotest 4 luo
Enrico Tassi [Fri, 14 Nov 2008 20:26:02 +0000 (20:26 +0000)]
test 4 luo

16 years ago...
Enrico Tassi [Fri, 14 Nov 2008 09:12:36 +0000 (09:12 +0000)]
...

16 years agobetter names
Enrico Tassi [Wed, 12 Nov 2008 15:04:41 +0000 (15:04 +0000)]
better names

16 years agodisambiguation for ng terms almost there
Enrico Tassi [Wed, 12 Nov 2008 12:42:08 +0000 (12:42 +0000)]
disambiguation for ng terms almost there

16 years agosome new exports
Enrico Tassi [Wed, 12 Nov 2008 12:41:23 +0000 (12:41 +0000)]
some new exports

16 years agonew meta added for ng_disambiguation
Enrico Tassi [Wed, 12 Nov 2008 12:41:02 +0000 (12:41 +0000)]
new meta added for ng_disambiguation

16 years agoexported disambiguate_thing
Enrico Tassi [Wed, 12 Nov 2008 12:09:52 +0000 (12:09 +0000)]
exported disambiguate_thing

16 years agooccurr check fixed
Enrico Tassi [Wed, 12 Nov 2008 11:11:12 +0000 (11:11 +0000)]
occurr check fixed

16 years agomore printings
Enrico Tassi [Wed, 12 Nov 2008 11:09:27 +0000 (11:09 +0000)]
more printings

16 years agolast fixes
Enrico Tassi [Tue, 11 Nov 2008 19:33:11 +0000 (19:33 +0000)]
last fixes