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

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

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

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

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

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

15 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

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

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

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

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

15 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

15 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

15 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

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

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

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

15 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

15 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

15 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

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

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

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

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

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

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

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

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

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

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

15 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

15 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

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

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

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

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

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

15 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.

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

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

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

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

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

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

15 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

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

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

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

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

15 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

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

15 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

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

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

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

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

15 years ago1. data structure for lables is now more strict
Claudio Sacerdoti Coen [Tue, 11 Nov 2008 18:04:02 +0000 (18:04 +0000)]
1. data structure for lables is now more strict
2. phase 3 completed (with a test)
3. simple optimizer for redundant jumps implemented

15 years ago- we now use a streaming architecture (run time gain: 11 secs)
Ferruccio Guidi [Tue, 11 Nov 2008 17:05:12 +0000 (17:05 +0000)]
- we now use a streaming architecture (run time gain: 11 secs)
- we added some time stamp support

15 years agoauto-param "size" missing
Claudio Sacerdoti Coen [Sun, 9 Nov 2008 10:27:38 +0000 (10:27 +0000)]
auto-param "size" missing

15 years agodebug=false
Andrea Asperti [Fri, 7 Nov 2008 17:03:17 +0000 (17:03 +0000)]
debug=false

15 years agoSignature_of has been closed with respect to constructors.
Andrea Asperti [Fri, 7 Nov 2008 16:55:37 +0000 (16:55 +0000)]
Signature_of has been closed with respect to constructors.

15 years agoThe signature in "retrieve equations" must be extended with the equality if
Andrea Asperti [Fri, 7 Nov 2008 16:53:55 +0000 (16:53 +0000)]
The signature in "retrieve equations" must be extended with the equality if
not already there, otherwise it may hardly find any equation.

15 years agosome other simplification
Enrico Tassi [Fri, 7 Nov 2008 14:31:25 +0000 (14:31 +0000)]
some other simplification

15 years agoordered_set simplified
Enrico Tassi [Fri, 7 Nov 2008 10:27:20 +0000 (10:27 +0000)]
ordered_set simplified

15 years agoexercise ready
Enrico Tassi [Fri, 7 Nov 2008 09:05:48 +0000 (09:05 +0000)]
exercise ready

15 years agoexercise ready
Enrico Tassi [Thu, 6 Nov 2008 20:03:39 +0000 (20:03 +0000)]
exercise ready

15 years agoalmost there
Enrico Tassi [Thu, 6 Nov 2008 19:42:37 +0000 (19:42 +0000)]
almost there

15 years ago...
Claudio Sacerdoti Coen [Thu, 6 Nov 2008 18:06:15 +0000 (18:06 +0000)]
...

15 years agoFirst attempts at the third phase.
Claudio Sacerdoti Coen [Thu, 6 Nov 2008 17:56:57 +0000 (17:56 +0000)]
First attempts at the third phase.

15 years agoadded some news
Enrico Tassi [Thu, 6 Nov 2008 16:47:35 +0000 (16:47 +0000)]
added some news

15 years agoalmost ok
Enrico Tassi [Thu, 6 Nov 2008 16:44:25 +0000 (16:44 +0000)]
almost ok

15 years agonatural deduction support and example split, seems to almost work.
Enrico Tassi [Thu, 6 Nov 2008 16:19:04 +0000 (16:19 +0000)]
natural deduction support and example split, seems to almost work.

15 years agodo not erase sorts
Enrico Tassi [Thu, 6 Nov 2008 14:06:00 +0000 (14:06 +0000)]
do not erase sorts

15 years agobetter error messages. sorts are compared using whd
Enrico Tassi [Thu, 6 Nov 2008 14:05:33 +0000 (14:05 +0000)]
better error messages. sorts are compared using whd

15 years agoEvil case fixed, the coulde should be more readable
Enrico Tassi [Thu, 6 Nov 2008 14:04:51 +0000 (14:04 +0000)]
Evil case fixed, the coulde should be more readable

15 years agoremoved empty lines
Enrico Tassi [Thu, 6 Nov 2008 14:04:21 +0000 (14:04 +0000)]
removed empty lines

15 years agothe passive set and passive list are expected to have the same cardinality, that...
Enrico Tassi [Thu, 6 Nov 2008 09:39:29 +0000 (09:39 +0000)]
the passive set and passive list are expected to have the same cardinality, that was was some bad reason not always the case

15 years agofixed scripts
Enrico Tassi [Thu, 6 Nov 2008 09:36:23 +0000 (09:36 +0000)]
fixed scripts

15 years agostill some glitches, but reaching a decent state
Enrico Tassi [Wed, 5 Nov 2008 22:46:24 +0000 (22:46 +0000)]
still some glitches, but reaching a decent state

15 years agousing the new by foo we proved semantics
Enrico Tassi [Wed, 5 Nov 2008 21:31:01 +0000 (21:31 +0000)]
using the new by foo we proved semantics

15 years agonew internal flags for auto:
Enrico Tassi [Wed, 5 Nov 2008 21:29:05 +0000 (21:29 +0000)]
new internal flags for auto:
- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)

15 years agoduplicate entry in menv avoided
Enrico Tassi [Wed, 5 Nov 2008 21:27:18 +0000 (21:27 +0000)]
duplicate entry in menv avoided

15 years agofixed script to use auto depth=4
Enrico Tassi [Wed, 5 Nov 2008 07:37:22 +0000 (07:37 +0000)]
fixed script to use auto depth=4

15 years agoeliminazione di un passaggio di transitività in ast2astfe
Enrico Tassi [Tue, 4 Nov 2008 15:23:36 +0000 (15:23 +0000)]
eliminazione di un passaggio di transitività in ast2astfe
dimostrazione di un assioma in env2flatenv

15 years agoCalling unification instead of matching when checking for subsumption
Andrea Asperti [Tue, 4 Nov 2008 15:13:34 +0000 (15:13 +0000)]
Calling unification instead of matching when checking for subsumption
might instantiate the goal with variables in table (while they are supposed
to be disjoint).