]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years ago- added src_root build time configuration value
Stefano Zacchiroli [Thu, 23 Feb 2006 21:31:23 +0000 (21:31 +0000)]
- added src_root build time configuration value
- added the disclaimer "ComponentsConf should not be here"

18 years agoinformation on current compilation state added in each file
Ferruccio Guidi [Thu, 23 Feb 2006 18:15:29 +0000 (18:15 +0000)]
information on current compilation state added in each file

18 years ago64 "change" here and there in the library are now simplify/unfold as they
Claudio Sacerdoti Coen [Thu, 23 Feb 2006 13:16:39 +0000 (13:16 +0000)]
64 "change" here and there in the library are now simplify/unfold as they
should have been. This has been possible because of some bugs fixed.

18 years agoDuring simplify, reduction of the argument of a Fix and of a MutCase is now
Claudio Sacerdoti Coen [Thu, 23 Feb 2006 13:13:04 +0000 (13:13 +0000)]
During simplify, reduction of the argument of a Fix and of a MutCase is now
performed using simplify. (It used to be performed by whd).
Pros: sometimes you should get simpler terms (but not so far)
Cons: sometimes simplification could simplify less than expected (but not so far)

18 years agoimproved comment of HExtlib.find
Stefano Zacchiroli [Wed, 22 Feb 2006 23:22:09 +0000 (23:22 +0000)]
improved comment of HExtlib.find

18 years ago- ensure simplify_deps exists when invoked
Stefano Zacchiroli [Wed, 22 Feb 2006 22:58:13 +0000 (22:58 +0000)]
- ensure simplify_deps exists when invoked
- added a SIMPLIFYDEPS variable to change its location

18 years agomoved initial (i.e. empty) lexiconEngine status to lexiconEngine from
Stefano Zacchiroli [Wed, 22 Feb 2006 22:39:47 +0000 (22:39 +0000)]
moved initial (i.e. empty) lexiconEngine status to lexiconEngine from
lexiconSync

18 years agosimplify used in place of change
Claudio Sacerdoti Coen [Wed, 22 Feb 2006 21:50:00 +0000 (21:50 +0000)]
simplify used in place of change

18 years agoBug fixed in simplify: delta expansion of constants applied to more arguments
Claudio Sacerdoti Coen [Wed, 22 Feb 2006 21:17:16 +0000 (21:17 +0000)]
Bug fixed in simplify: delta expansion of constants applied to more arguments
than head lambda abstractions was always performed (even if no "interesting"
reduction took place).

18 years agochanged structure of the generated utf8MacroTable.ml file so that it can be
Stefano Zacchiroli [Wed, 22 Feb 2006 14:39:11 +0000 (14:39 +0000)]
changed structure of the generated utf8MacroTable.ml file so that it can be
compiled with ocamlopt avoiding Stack_overflow

18 years agoMissing -I ../.. added.
Claudio Sacerdoti Coen [Wed, 22 Feb 2006 14:13:31 +0000 (14:13 +0000)]
Missing -I ../.. added.

18 years agoFirst part of bug #152 (unable to exit from Matita) solved.
Claudio Sacerdoti Coen [Wed, 22 Feb 2006 14:00:21 +0000 (14:00 +0000)]
First part of bug #152 (unable to exit from Matita) solved.

18 years agoOrder of compilation of the modules fixed.
Claudio Sacerdoti Coen [Wed, 22 Feb 2006 13:56:15 +0000 (13:56 +0000)]
Order of compilation of the modules fixed.

18 years agoCoercions are now hidden by default in termAcicContent.ml.
Claudio Sacerdoti Coen [Tue, 21 Feb 2006 18:23:18 +0000 (18:23 +0000)]
Coercions are now hidden by default in termAcicContent.ml.

18 years agoCoercions are now hidden by default (in termAcicContent.ml)
Claudio Sacerdoti Coen [Tue, 21 Feb 2006 18:22:12 +0000 (18:22 +0000)]
Coercions are now hidden by default (in termAcicContent.ml)

18 years agopack_coercion used to avoid packing n-ary coercions where n > 2.
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 16:37:36 +0000 (16:37 +0000)]
pack_coercion used to avoid packing n-ary coercions where n > 2.
Fixed.

18 years agoStupid bug fixed.
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 16:36:28 +0000 (16:36 +0000)]
Stupid bug fixed.

18 years agoPacking of implicit coercions must be also performed as soon as an object (or proof...
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 15:55:35 +0000 (15:55 +0000)]
Packing of implicit coercions must be also performed as soon as an object (or proof status) is created.

18 years agoFinished one lemma (after many bug fixes here and there).
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 15:05:37 +0000 (15:05 +0000)]
Finished one lemma (after many bug fixes here and there).

18 years agoBug fixed: rewrite > t where t had occurrences of metavariables in it could
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 14:47:00 +0000 (14:47 +0000)]
Bug fixed: rewrite > t where t had occurrences of metavariables in it could
fail because of a missing apply_subst.

18 years agoLocalization bug fixed.
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 13:59:46 +0000 (13:59 +0000)]
Localization bug fixed.

18 years agoSome more implicit coercions here and there.
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 13:47:32 +0000 (13:47 +0000)]
Some more implicit coercions here and there.

18 years agoBug fixed in pack_coercions_obj. The context of the metas in the metasenv of
Claudio Sacerdoti Coen [Mon, 20 Feb 2006 13:24:01 +0000 (13:24 +0000)]
Bug fixed in pack_coercions_obj. The context of the metas in the metasenv of
the CurrentProof was not translated correctly.

18 years agoclass definition updated (but buggy now)
Ferruccio Guidi [Mon, 20 Feb 2006 11:58:44 +0000 (11:58 +0000)]
class definition updated (but buggy now)

18 years agoBug fixed: the source and target of declared parametric coercions used to
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 19:31:28 +0000 (19:31 +0000)]
Bug fixed: the source and target of declared parametric coercions used to
be URIs of the inductive block instead of being URIs of single inductive
types or constructors.

18 years agoTrivial bug fixed in the merging of polymorphic coercions.
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 18:20:02 +0000 (18:20 +0000)]
Trivial bug fixed in the merging of polymorphic coercions.

18 years agoBug fixed in insertion of parametric coercions.
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 15:53:16 +0000 (15:53 +0000)]
Bug fixed in insertion of parametric coercions.
To fix the bug, the CoercGraph.look_for_coercion now returns a term saturated
with Cic.Implicits. As usual, remember to refine the term before further usage.

18 years agoMore refinement errors localized.
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 14:33:42 +0000 (14:33 +0000)]
More refinement errors localized.

18 years agoMore refinement errors localized.
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 12:22:18 +0000 (12:22 +0000)]
More refinement errors localized.

18 years agoBug fixed: the wrong exception was enriched, breaking the invariant that
Claudio Sacerdoti Coen [Sat, 18 Feb 2006 11:33:05 +0000 (11:33 +0000)]
Bug fixed: the wrong exception was enriched, breaking the invariant that
only unlocalized exceptions can be enriched.

18 years agoSys.command -> Unix.system
Enrico Tassi [Fri, 17 Feb 2006 15:40:09 +0000 (15:40 +0000)]
Sys.command -> Unix.system

18 years agotentative speedup not coercion-packing the proof after every step
Enrico Tassi [Fri, 17 Feb 2006 14:53:33 +0000 (14:53 +0000)]
tentative speedup not coercion-packing the proof after every step

18 years agoadded support for "polymorphic" coercions
Enrico Tassi [Wed, 15 Feb 2006 13:04:35 +0000 (13:04 +0000)]
added support for "polymorphic" coercions

18 years agofix
Enrico Tassi [Wed, 15 Feb 2006 11:49:03 +0000 (11:49 +0000)]
fix

18 years agofix
Enrico Tassi [Wed, 15 Feb 2006 08:38:50 +0000 (08:38 +0000)]
fix

18 years agofix
Enrico Tassi [Tue, 14 Feb 2006 20:33:17 +0000 (20:33 +0000)]
fix

18 years agofix
Enrico Tassi [Tue, 14 Feb 2006 20:25:18 +0000 (20:25 +0000)]
fix

18 years agoadded info on how to create the dumps
Stefano Zacchiroli [Tue, 14 Feb 2006 18:45:50 +0000 (18:45 +0000)]
added info on how to create the dumps

18 years agoadded snapshot of the coq exportation metadata
Stefano Zacchiroli [Tue, 14 Feb 2006 18:38:45 +0000 (18:38 +0000)]
added snapshot of the coq exportation metadata

18 years agotentative fix
Enrico Tassi [Tue, 14 Feb 2006 15:36:10 +0000 (15:36 +0000)]
tentative fix

18 years agoreverted orrible but correct syntax
Enrico Tassi [Tue, 14 Feb 2006 12:40:49 +0000 (12:40 +0000)]
reverted orrible but correct syntax

18 years agofixed syntax
Enrico Tassi [Tue, 14 Feb 2006 12:18:44 +0000 (12:18 +0000)]
fixed syntax

18 years agoRecapitalization of sect_tactics.xml
Claudio Sacerdoti Coen [Thu, 9 Feb 2006 16:49:02 +0000 (16:49 +0000)]
Recapitalization of sect_tactics.xml

18 years agoSome fixes in the documentation of the tactics.
Claudio Sacerdoti Coen [Thu, 9 Feb 2006 16:30:20 +0000 (16:30 +0000)]
Some fixes in the documentation of the tactics.

18 years agoA few intros_spec were missing here and there.
Claudio Sacerdoti Coen [Thu, 9 Feb 2006 16:27:50 +0000 (16:27 +0000)]
A few intros_spec were missing here and there.

18 years agoTypo fixed.
Claudio Sacerdoti Coen [Thu, 9 Feb 2006 16:16:18 +0000 (16:16 +0000)]
Typo fixed.

18 years agoMost of the tactics are now documented.
Claudio Sacerdoti Coen [Thu, 9 Feb 2006 16:14:18 +0000 (16:14 +0000)]
Most of the tactics are now documented.

18 years agocompleted installation instructions
Stefano Zacchiroli [Thu, 9 Feb 2006 00:19:56 +0000 (00:19 +0000)]
completed installation instructions

18 years agoEven more tactics documented.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 17:55:19 +0000 (17:55 +0000)]
Even more tactics documented.

18 years agoNew tactics (badly) documented.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 17:43:11 +0000 (17:43 +0000)]
New tactics (badly) documented.

18 years agoimplemented "install" target
Stefano Zacchiroli [Wed, 8 Feb 2006 17:15:07 +0000 (17:15 +0000)]
implemented "install" target

18 years agobuild temporary library in software/matita/.matita (instead of software/.matita)
Stefano Zacchiroli [Wed, 8 Feb 2006 17:14:49 +0000 (17:14 +0000)]
build temporary library in software/matita/.matita (instead of software/.matita)

18 years agoremoved duplicate copy of AUTHORS
Stefano Zacchiroli [Wed, 8 Feb 2006 17:14:19 +0000 (17:14 +0000)]
removed duplicate copy of AUTHORS

18 years agoinstall in /usr/local/matita/
Stefano Zacchiroli [Wed, 8 Feb 2006 17:14:06 +0000 (17:14 +0000)]
install in /usr/local/matita/

18 years agoexpand SRCROOT (is needed by matita/Makefile)
Stefano Zacchiroli [Wed, 8 Feb 2006 17:12:47 +0000 (17:12 +0000)]
expand SRCROOT (is needed by matita/Makefile)

18 years agobumped year
Stefano Zacchiroli [Wed, 8 Feb 2006 17:12:22 +0000 (17:12 +0000)]
bumped year

18 years agoNicer index for tactics in Yelp.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 16:51:43 +0000 (16:51 +0000)]
Nicer index for tactics in Yelp.

18 years agoported to the docbook "book"
Stefano Zacchiroli [Wed, 8 Feb 2006 16:49:55 +0000 (16:49 +0000)]
ported to the docbook "book"

18 years agoStrange fix (for a yelp bug?)
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 16:40:25 +0000 (16:40 +0000)]
Strange fix (for a yelp bug?)

18 years agoFrom article to book
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 16:36:39 +0000 (16:36 +0000)]
From article to book

18 years agocomment out an incomplete proof
Stefano Zacchiroli [Wed, 8 Feb 2006 15:35:08 +0000 (15:35 +0000)]
comment out an incomplete proof

18 years agoMore tactics documented.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 14:27:37 +0000 (14:27 +0000)]
More tactics documented.

18 years agoSeveral more tactics documented.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 14:15:34 +0000 (14:15 +0000)]
Several more tactics documented.

18 years agoNever implemented tactics compare and decide equality purged from the code.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 13:38:43 +0000 (13:38 +0000)]
Never implemented tactics compare and decide equality purged from the code.

18 years agoadded title to sliced htmls
Stefano Zacchiroli [Wed, 8 Feb 2006 12:54:56 +0000 (12:54 +0000)]
added title to sliced htmls

18 years agoadded pretty printing of generated xml files via xmllint --format
Stefano Zacchiroli [Wed, 8 Feb 2006 12:54:42 +0000 (12:54 +0000)]
added pretty printing of generated xml files via xmllint --format

18 years agoadded generation of .html and .txt version of manual parts
Stefano Zacchiroli [Wed, 8 Feb 2006 12:38:11 +0000 (12:38 +0000)]
added generation of .html and .txt version of manual parts

18 years ago- removed old commented code
Stefano Zacchiroli [Wed, 8 Feb 2006 12:33:08 +0000 (12:33 +0000)]
- removed old commented code
- added copyright notice

18 years agoHelp for the first two tactics.
Claudio Sacerdoti Coen [Wed, 8 Feb 2006 10:55:57 +0000 (10:55 +0000)]
Help for the first two tactics.

18 years agoadded splitting engine for .html generated by docbook -> xhtml conversion
Stefano Zacchiroli [Wed, 8 Feb 2006 10:34:37 +0000 (10:34 +0000)]
added splitting engine for .html generated by docbook -> xhtml conversion

18 years agono more dummy names for building the library in distributed tarballs
Stefano Zacchiroli [Wed, 8 Feb 2006 10:33:59 +0000 (10:33 +0000)]
no more dummy names for building the library in distributed tarballs

18 years ago"sec_" prefix for section IDs
Stefano Zacchiroli [Tue, 7 Feb 2006 23:08:27 +0000 (23:08 +0000)]
"sec_" prefix for section IDs

18 years agoAdded a few basic definitions of subgroups and left cosets (together with
Claudio Sacerdoti Coen [Tue, 7 Feb 2006 18:26:27 +0000 (18:26 +0000)]
Added a few basic definitions of subgroups and left cosets (together with
their extreme notation!)

18 years agoadded instructions (some gaps still to be filled in, notably: ./configure
Stefano Zacchiroli [Tue, 7 Feb 2006 17:54:41 +0000 (17:54 +0000)]
added instructions (some gaps still to be filled in, notably: ./configure
parameters and instructions on how to create the mysql database)

18 years agowritten install section up to build requirements
Stefano Zacchiroli [Tue, 7 Feb 2006 17:31:38 +0000 (17:31 +0000)]
written install section up to build requirements

18 years agochanged location of version.txt
Stefano Zacchiroli [Tue, 7 Feb 2006 15:13:41 +0000 (15:13 +0000)]
changed location of version.txt

18 years ago- moved version.txt.in to the help dir
Stefano Zacchiroli [Tue, 7 Feb 2006 14:54:25 +0000 (14:54 +0000)]
- moved version.txt.in to the help dir
- added Makefile to generate xhtml and pdf from the docbook manual

18 years agoreshaped manual
Stefano Zacchiroli [Tue, 7 Feb 2006 13:39:52 +0000 (13:39 +0000)]
reshaped manual

18 years ago- use the best matitamake to build the library on dist
Stefano Zacchiroli [Tue, 7 Feb 2006 10:54:15 +0000 (10:54 +0000)]
- use the best matitamake to build the library on dist
- renamed dist targets so that they are distinguishable and not callable in
  when developing matita

18 years agofill DISTRIBUTED value on dist
Stefano Zacchiroli [Tue, 7 Feb 2006 10:53:20 +0000 (10:53 +0000)]
fill DISTRIBUTED value on dist

18 years agoremoved useless grepping -v
Stefano Zacchiroli [Tue, 7 Feb 2006 10:53:01 +0000 (10:53 +0000)]
removed useless grepping -v

18 years ago- factorization of the recursive rule
Stefano Zacchiroli [Tue, 7 Feb 2006 10:52:35 +0000 (10:52 +0000)]
- factorization of the recursive rule
- added "library" target to build the stdlib when distributed
- implemented "distcheck" target

18 years agoadded configure time values SRCROOT and DISTRIBUTED
Stefano Zacchiroli [Tue, 7 Feb 2006 10:51:44 +0000 (10:51 +0000)]
added configure time values SRCROOT and DISTRIBUTED

18 years agofactorization of the recursive rule
Stefano Zacchiroli [Tue, 7 Feb 2006 10:51:02 +0000 (10:51 +0000)]
factorization of the recursive rule

18 years agoadded Matitamake interface
Stefano Zacchiroli [Mon, 6 Feb 2006 18:30:11 +0000 (18:30 +0000)]
added Matitamake interface

18 years agoabsolute path and factorization for matita.basedir
Stefano Zacchiroli [Mon, 6 Feb 2006 17:22:11 +0000 (17:22 +0000)]
absolute path and factorization for matita.basedir

18 years ago- changed semantics of "init": now it is idempotent
Stefano Zacchiroli [Mon, 6 Feb 2006 17:21:39 +0000 (17:21 +0000)]
- changed semantics of "init": now it is idempotent
- added support for "-v" flag printing "make" command line
- minor change: lazy discovering of whether we are ".opt" or not

18 years agouse matita.verbosity instead of matita.quiet
Stefano Zacchiroli [Mon, 6 Feb 2006 17:19:52 +0000 (17:19 +0000)]
use matita.verbosity instead of matita.quiet

18 years ago- uniformed command line handling of matitamake with that of other matita tools
Stefano Zacchiroli [Mon, 6 Feb 2006 17:19:28 +0000 (17:19 +0000)]
- uniformed command line handling of matitamake with that of other matita tools
- changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1
  unit
- added "-v" flag: it increase the "matita.verbosity" value by 1
- "matita.quiet" is no longer in use

18 years agohelp path is no longer hard coded but relative to runtime base dir
Stefano Zacchiroli [Mon, 6 Feb 2006 17:17:10 +0000 (17:17 +0000)]
help path is no longer hard coded but relative to runtime base dir

18 years agofixed tactic ids to include a "tac_" prefix
Stefano Zacchiroli [Mon, 6 Feb 2006 17:16:40 +0000 (17:16 +0000)]
fixed tactic ids to include a "tac_" prefix

18 years ago- bugfix: pass -conffile to matitamake
Stefano Zacchiroli [Mon, 6 Feb 2006 17:15:30 +0000 (17:15 +0000)]
- bugfix: pass -conffile to matitamake
- more quiet feedback during compilation of stdlib

18 years agoBasic facts about group morphisms.
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 14:00:18 +0000 (14:00 +0000)]
Basic facts about group morphisms.

18 years agomoved mathql/ under software/
Stefano Zacchiroli [Mon, 6 Feb 2006 11:33:01 +0000 (11:33 +0000)]
moved mathql/ under software/

18 years agofirst sketch of the documentation (to be used by yelp)
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 11:22:27 +0000 (11:22 +0000)]
first sketch of the documentation (to be used by yelp)

18 years agos/ocaml/components/ in the "tag" target
Stefano Zacchiroli [Mon, 6 Feb 2006 11:18:22 +0000 (11:18 +0000)]
s/ocaml/components/ in the "tag" target

18 years ago* groups splitted into groups and finite_groups
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 10:34:27 +0000 (10:34 +0000)]
* groups splitted into groups and finite_groups
* a few lemmas added to groups

18 years agoremoved a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow...
Claudio Sacerdoti Coen [Mon, 6 Feb 2006 10:28:11 +0000 (10:28 +0000)]
removed a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow... mah...

18 years agotermine bacato.
Andrea Asperti [Mon, 6 Feb 2006 09:58:37 +0000 (09:58 +0000)]
termine bacato.

18 years agofixed usage of matita.auto_disambiguation
Andrea Asperti [Mon, 6 Feb 2006 09:40:31 +0000 (09:40 +0000)]
fixed usage of matita.auto_disambiguation