]> matita.cs.unibo.it Git - helm.git/log
helm.git
18 years agoBug fixed that made theory rendering bugged after visiting a whelp search page.
Claudio Sacerdoti Coen [Thu, 1 Jun 2006 09:57:50 +0000 (09:57 +0000)]
Bug fixed that made theory rendering bugged after visiting a whelp search page.

18 years agobugfix: rely on byte count instead of mixing byte and character count
Stefano Zacchiroli [Thu, 1 Jun 2006 09:32:12 +0000 (09:32 +0000)]
bugfix: rely on byte count instead of mixing byte and character count

18 years agoSubsumption_subst must be applied to the initial proof before passing
Andrea Asperti [Thu, 1 Jun 2006 07:31:25 +0000 (07:31 +0000)]
Subsumption_subst must be applied to the initial proof before passing
it to build_proof_goal.

18 years agoSigma algebras and measurable maps defined.
Claudio Sacerdoti Coen [Wed, 31 May 2006 17:12:12 +0000 (17:12 +0000)]
Sigma algebras and measurable maps defined.

18 years agoCommitted a first experiment in the formalization of Lebesgue dominated
Claudio Sacerdoti Coen [Wed, 31 May 2006 15:54:25 +0000 (15:54 +0000)]
Committed a first experiment in the formalization of Lebesgue dominated
convergence theorem: basic set theory and classical topology definitions.

18 years ago\n restored
Enrico Tassi [Wed, 31 May 2006 13:54:57 +0000 (13:54 +0000)]
\n restored

18 years agofixed proofs, contextualization should now work.
Enrico Tassi [Wed, 31 May 2006 13:54:36 +0000 (13:54 +0000)]
fixed proofs, contextualization should now work.
the empty context is not a term with an open (Rel 1), but a
a term with a (Cic.Implicit(Some `Hole)) so that it can't bw confused with a
Rel to the last Hypothesis.

18 years ago1. the default encoding for the stylesheets is now UTF8
Claudio Sacerdoti Coen [Tue, 30 May 2006 16:50:33 +0000 (16:50 +0000)]
1. the default encoding for the stylesheets is now UTF8
2. committed a few changes in search.xsl that had never been committed before

18 years agomatita.txt updated
Claudio Sacerdoti Coen [Tue, 30 May 2006 14:56:58 +0000 (14:56 +0000)]
matita.txt updated

18 years agoBug fixed: theories were handled as base uris, not as uris of files.
Claudio Sacerdoti Coen [Tue, 30 May 2006 14:30:19 +0000 (14:30 +0000)]
Bug fixed: theories were handled as base uris, not as uris of files.

18 years agoletin are now sorted properly.
Enrico Tassi [Tue, 30 May 2006 11:50:51 +0000 (11:50 +0000)]
letin are now sorted properly.

18 years agofixed proof generation again
Enrico Tassi [Tue, 30 May 2006 10:44:55 +0000 (10:44 +0000)]
fixed proof generation again

18 years agouse the proper top level function to parse terms
Claudio Sacerdoti Coen [Tue, 30 May 2006 10:33:42 +0000 (10:33 +0000)]
use the proper top level function to parse terms

18 years agoZACK: export a top level function for parsing terms, it can't be bypassed due to...
Claudio Sacerdoti Coen [Tue, 30 May 2006 10:22:57 +0000 (10:22 +0000)]
ZACK: export a top level function for parsing terms, it can't be bypassed due to the Obj.magic trick

18 years ago...
Enrico Tassi [Tue, 30 May 2006 09:26:15 +0000 (09:26 +0000)]
...

18 years agoA -> Univ
Enrico Tassi [Tue, 30 May 2006 09:19:14 +0000 (09:19 +0000)]
A -> Univ

18 years agocanonical and contextualize_rewrites are back, they seem to work now...
Enrico Tassi [Tue, 30 May 2006 09:09:37 +0000 (09:09 +0000)]
canonical and contextualize_rewrites are back, they seem to work now...

18 years agothe function to create on the fly a symmetry step has been moved to equality
Enrico Tassi [Tue, 30 May 2006 08:59:27 +0000 (08:59 +0000)]
the function to create on the fly a symmetry step has been moved to equality

18 years agoadded our poor results to CASC 2005
Enrico Tassi [Tue, 30 May 2006 08:42:24 +0000 (08:42 +0000)]
added our poor results to CASC 2005

18 years agoZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:14:33 +0000 (08:14 +0000)]
ZACK: ported to the latest ocaml-http API

18 years agoZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:13:55 +0000 (08:13 +0000)]
ZACK: ported to the latest ocaml-http API

18 years agoported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:11:37 +0000 (08:11 +0000)]
ported to the latest ocaml-http API

18 years agoZACK: ported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:10:47 +0000 (08:10 +0000)]
ZACK: ported to the latest ocaml-http API

18 years agoported to the latest ocaml-http API
Claudio Sacerdoti Coen [Tue, 30 May 2006 08:04:50 +0000 (08:04 +0000)]
ported to the latest ocaml-http API

18 years agobugfix: when creating a daemon spec _use_ the auto_close value passed as argument...
Stefano Zacchiroli [Tue, 30 May 2006 07:58:45 +0000 (07:58 +0000)]
bugfix: when creating a daemon spec _use_ the auto_close value passed as argument instead of ignoring it

18 years ago- removed Http_daemon.{start,start\}
Stefano Zacchiroli [Mon, 29 May 2006 20:52:22 +0000 (20:52 +0000)]
- removed Http_daemon.{start,start\}

18 years agoadded some logs
Enrico Tassi [Mon, 29 May 2006 20:44:57 +0000 (20:44 +0000)]
added some logs

18 years agofix
Enrico Tassi [Mon, 29 May 2006 20:41:16 +0000 (20:41 +0000)]
fix

18 years agocommitted the base utils for TPTP processing
Enrico Tassi [Mon, 29 May 2006 20:40:35 +0000 (20:40 +0000)]
committed the base utils for TPTP processing

18 years agoadded finally function
Stefano Zacchiroli [Mon, 29 May 2006 20:33:30 +0000 (20:33 +0000)]
added finally function

18 years agoprofilings are printed
Enrico Tassi [Mon, 29 May 2006 20:32:58 +0000 (20:32 +0000)]
profilings are printed

18 years ago- proofs by subsumption now add a symmetry step if needed
Enrico Tassi [Mon, 29 May 2006 20:29:21 +0000 (20:29 +0000)]
- proofs by subsumption now add a symmetry step if needed
- a little optimization for Equality.depend (just to aviod te exponenetial
  factor, but should be made faster)
- restored names in Lambda abstraction that give infos about the step they
  represent

18 years agoforces bash as Makefile SHELL
Stefano Zacchiroli [Mon, 29 May 2006 20:27:57 +0000 (20:27 +0000)]
forces bash as Makefile SHELL

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:36:36 +0000 (17:36 +0000)]
ensure connections get closed after having been served

18 years agolowered debugging level
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:34:16 +0000 (17:34 +0000)]
lowered debugging level

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:24:43 +0000 (17:24 +0000)]
ensure connections get closed after having been served

18 years agoOCAMLPATH is not overrid if already defined
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:20:16 +0000 (17:20 +0000)]
OCAMLPATH is not overrid if already defined

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:13:03 +0000 (17:13 +0000)]
ensure connections get closed after having been served

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:10:14 +0000 (17:10 +0000)]
ensure connections get closed after having been served

18 years agobugfix:
Claudio Sacerdoti Coen [Mon, 29 May 2006 17:03:24 +0000 (17:03 +0000)]
bugfix:
- properties where applied and then discarded
- useless assert false removed

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 16:54:47 +0000 (16:54 +0000)]
ensure connections get closed after having been served

18 years agoensure connections get closed after having been served
Claudio Sacerdoti Coen [Mon, 29 May 2006 16:54:36 +0000 (16:54 +0000)]
ensure connections get closed after having been served

18 years agobug fix: use an (un)marshaller for get_opt instead of a getter
Claudio Sacerdoti Coen [Mon, 29 May 2006 14:12:40 +0000 (14:12 +0000)]
bug fix: use an (un)marshaller for get_opt instead of a getter

18 years agoOCAMLPATH is no longer overrid if already set in current environment
Stefano Zacchiroli [Mon, 29 May 2006 13:49:53 +0000 (13:49 +0000)]
OCAMLPATH is no longer overrid if already set in current environment

18 years agoBug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed...
Claudio Sacerdoti Coen [Mon, 29 May 2006 13:41:52 +0000 (13:41 +0000)]
Bug fixed in fresh_name_generator: the function used to fail on beta redexes. Fixed trivially without
introducing yet another whd.

18 years agoadded (TODO) section on tacticals)
Stefano Zacchiroli [Mon, 29 May 2006 11:56:28 +0000 (11:56 +0000)]
added (TODO) section on tacticals)

18 years agoweak equality on meta used when replacing.
Enrico Tassi [Sun, 28 May 2006 16:10:26 +0000 (16:10 +0000)]
weak equality on meta used when replacing.
updated to the new goal_proof

18 years agoadded the rule field to goal_proof.
Enrico Tassi [Sun, 28 May 2006 16:09:00 +0000 (16:09 +0000)]
added the rule field to goal_proof.
fixed the SupL proof generation (but I think the fix should not be here)

18 years ago- fixed a bug in unification (not sure in the right way)
Enrico Tassi [Sun, 28 May 2006 16:07:33 +0000 (16:07 +0000)]
- fixed a bug in unification (not sure in the right way)

18 years agoCALS tables enriched to make (crappy) docbook stylesheets happy.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:58:47 +0000 (15:58 +0000)]
CALS tables enriched to make (crappy) docbook stylesheets happy.

18 years agoDocumentation fixed.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:39:29 +0000 (15:39 +0000)]
Documentation fixed.

18 years agoNew documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 15:14:41 +0000 (15:14 +0000)]
New documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 14:18:09 +0000 (14:18 +0000)]
More documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Fri, 26 May 2006 13:41:55 +0000 (13:41 +0000)]
More documentation.

18 years agoRecently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
Claudio Sacerdoti Coen [Fri, 26 May 2006 12:46:32 +0000 (12:46 +0000)]
Recently introduced bug in CicRefine.eat_prods fixed: a whd was now missing.
Added a test to verify the performances of refinement.

18 years agoSyntax highlighting for focus/unfocus
Claudio Sacerdoti Coen [Fri, 26 May 2006 12:38:42 +0000 (12:38 +0000)]
Syntax highlighting for focus/unfocus

18 years agoGreat optimization for eat_prods: if the type of the head of the application is meta_...
Claudio Sacerdoti Coen [Fri, 26 May 2006 11:18:47 +0000 (11:18 +0000)]
Great optimization for eat_prods: if the type of the head of the application is meta_closed,
the construction of the spine of Prods and relative unification is skipped.

18 years ago1) variables occurring only in proofs anre not relocated
Andrea Asperti [Fri, 26 May 2006 11:08:29 +0000 (11:08 +0000)]
1) variables occurring only in proofs anre not relocated
2) during unification the resulting metasenv is cleaned of duplicates
   (duplicates can only be variables in proofs, not in left/right)

18 years agoProfiling code removed.
Claudio Sacerdoti Coen [Fri, 26 May 2006 10:10:39 +0000 (10:10 +0000)]
Profiling code removed.

18 years agoBug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".
Andrea Asperti [Fri, 26 May 2006 08:03:20 +0000 (08:03 +0000)]
Bug fixed: the syntax "?n" used to be broken. It tried a string_of_int "?n".

18 years agoMore documentation.
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:37:27 +0000 (17:37 +0000)]
More documentation.

18 years agoMore documentation.
Claudio Sacerdoti Coen [Thu, 25 May 2006 17:13:58 +0000 (17:13 +0000)]
More documentation.

18 years agoMore doc
Claudio Sacerdoti Coen [Thu, 25 May 2006 14:33:13 +0000 (14:33 +0000)]
More doc

18 years agoadded a file useful to load all notation
Enrico Tassi [Thu, 25 May 2006 14:10:17 +0000 (14:10 +0000)]
added a file useful to load all notation
(use include' and not include).

18 years agoAdded debug menu item to restrict disambiguation to the first pass only.
Claudio Sacerdoti Coen [Thu, 25 May 2006 12:05:58 +0000 (12:05 +0000)]
Added debug menu item to restrict disambiguation to the first pass only.

18 years agoAxioms are not allowed with the syntax: "axiom name: type.".
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:24:34 +0000 (10:24 +0000)]
Axioms are not allowed with the syntax: "axiom name: type.".

18 years agosvn:ignore fixed (again)
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:05:22 +0000 (10:05 +0000)]
svn:ignore fixed (again)

18 years agosvn:ignore fixed
Claudio Sacerdoti Coen [Thu, 25 May 2006 10:04:39 +0000 (10:04 +0000)]
svn:ignore fixed

18 years agomatita.txt updated
Claudio Sacerdoti Coen [Thu, 25 May 2006 08:56:12 +0000 (08:56 +0000)]
matita.txt updated

18 years agoadded important comment
Andrea Asperti [Tue, 23 May 2006 12:07:36 +0000 (12:07 +0000)]
added important comment

18 years agofixed LetIn proofs
Andrea Asperti [Tue, 23 May 2006 11:56:39 +0000 (11:56 +0000)]
fixed LetIn proofs

18 years agoadded again stuff for profiling
Enrico Tassi [Tue, 23 May 2006 08:07:25 +0000 (08:07 +0000)]
added again stuff for profiling

18 years agoadded dependency on Str
Enrico Tassi [Tue, 23 May 2006 08:06:07 +0000 (08:06 +0000)]
added dependency on Str

18 years ago...
Enrico Tassi [Tue, 23 May 2006 08:05:09 +0000 (08:05 +0000)]
...

18 years agoadded stuff for profiling macros
Andrea Asperti [Tue, 23 May 2006 08:03:18 +0000 (08:03 +0000)]
added stuff for profiling macros

18 years ago- code cleanup, especialli in Indexing where all the goal related functions have
Enrico Tassi [Mon, 22 May 2006 15:06:42 +0000 (15:06 +0000)]
- code cleanup, especialli in Indexing where all the goal related functions have
  been revised
- proofs are now factorized with LetIn
- support for profiling

18 years agogeneration of existential variables fixed
Enrico Tassi [Sat, 20 May 2006 12:23:02 +0000 (12:23 +0000)]
generation of existential variables fixed

18 years agoremoved prerr_endline.
Enrico Tassi [Sat, 20 May 2006 12:20:55 +0000 (12:20 +0000)]
removed prerr_endline.

18 years agocommented out a line to help paramodulation.
Enrico Tassi [Sat, 20 May 2006 10:49:11 +0000 (10:49 +0000)]
commented out a line to help paramodulation.
now if 0 goals are open every tactic is vacuosly performed

18 years agofixed wrong calculation of free_metas
Enrico Tassi [Sat, 20 May 2006 10:42:04 +0000 (10:42 +0000)]
fixed wrong calculation of free_metas

18 years agoremoved a bad prerr_endline
Enrico Tassi [Sat, 20 May 2006 10:11:47 +0000 (10:11 +0000)]
removed a bad prerr_endline

18 years agoremoved prerr_endline
Enrico Tassi [Sat, 20 May 2006 10:08:43 +0000 (10:08 +0000)]
removed prerr_endline

18 years agoremovedx a prerr_endline
Enrico Tassi [Sat, 20 May 2006 10:07:01 +0000 (10:07 +0000)]
removedx a prerr_endline

18 years agofixed demodulation of goal
Enrico Tassi [Sat, 20 May 2006 10:05:27 +0000 (10:05 +0000)]
fixed demodulation of goal

18 years ago- metas_of_term moved to cicUtil
Enrico Tassi [Fri, 19 May 2006 12:19:04 +0000 (12:19 +0000)]
- metas_of_term moved to cicUtil
- fixed proof generation
- added again typechecking of generated proof

18 years agoexistential variables in goal supported
Enrico Tassi [Thu, 18 May 2006 11:06:40 +0000 (11:06 +0000)]
existential variables in goal supported

18 years agoported to ocaml 3.09.2
Stefano Zacchiroli [Wed, 17 May 2006 05:28:16 +0000 (05:28 +0000)]
ported to ocaml 3.09.2

18 years agoported to ocaml 3.09.2
Stefano Zacchiroli [Wed, 17 May 2006 05:17:54 +0000 (05:17 +0000)]
ported to ocaml 3.09.2

18 years agoported to ocaml 3.09.2
Stefano Zacchiroli [Wed, 17 May 2006 04:56:28 +0000 (04:56 +0000)]
ported to ocaml 3.09.2

18 years agodo not export .svn directories
Stefano Zacchiroli [Tue, 16 May 2006 23:07:46 +0000 (23:07 +0000)]
do not export .svn directories

18 years agotransition to ocaml 3.09.2
Stefano Zacchiroli [Tue, 16 May 2006 23:03:30 +0000 (23:03 +0000)]
transition to ocaml 3.09.2

18 years agofixed subsumption_aux
Enrico Tassi [Tue, 16 May 2006 15:17:51 +0000 (15:17 +0000)]
fixed subsumption_aux
- (merge_subst_if_possible no longer needed)
- fixed case of use_unification = true

18 years agoutf8_macros moved to syntax_extensions.
Enrico Tassi [Tue, 16 May 2006 08:29:31 +0000 (08:29 +0000)]
utf8_macros moved to syntax_extensions.
quoting for inline profiling added

18 years agofew fixes
Enrico Tassi [Tue, 16 May 2006 08:26:38 +0000 (08:26 +0000)]
few fixes

18 years agoCSC & Andrea patch to speedup the process: typeof called instead of Hashtbl lookup
Enrico Tassi [Tue, 16 May 2006 08:25:34 +0000 (08:25 +0000)]
CSC & Andrea patch to speedup the process: typeof called instead of Hashtbl lookup

18 years agomore profiling and less assertions
Enrico Tassi [Tue, 16 May 2006 08:23:42 +0000 (08:23 +0000)]
more profiling and less assertions

18 years agobetter exception
Enrico Tassi [Tue, 16 May 2006 08:22:10 +0000 (08:22 +0000)]
better exception

18 years agohashtbl on cic terms is a bit faster
Enrico Tassi [Tue, 16 May 2006 08:21:51 +0000 (08:21 +0000)]
hashtbl on cic terms is a bit faster

18 years ago- new given_clause
Enrico Tassi [Mon, 15 May 2006 14:54:35 +0000 (14:54 +0000)]
- new given_clause
- support for a set of goals in OR
- restored superposition_left (even if not called)

18 years agobetter way of generating multiple pages XHTML output
Stefano Zacchiroli [Sun, 14 May 2006 17:41:30 +0000 (17:41 +0000)]
better way of generating multiple pages XHTML output