]> matita.cs.unibo.it Git - helm.git/log
helm.git
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 agofixed typo
Enrico Tassi [Fri, 19 May 2006 08:24:02 +0000 (08:24 +0000)]
fixed typo

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 agofix
Enrico Tassi [Tue, 16 May 2006 13:10:12 +0000 (13:10 +0000)]
fix

18 years agofixed
Enrico Tassi [Tue, 16 May 2006 08:58:22 +0000 (08:58 +0000)]
fixed

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

18 years ago- Removed old proofs
Enrico Tassi [Sun, 14 May 2006 13:53:37 +0000 (13:53 +0000)]
- Removed old proofs
- Equality.ml splittend in to subst.ml and equality.ml, the former only for substs
- patch to kill passive generated from an active that is dropped
- fixed deep subsumption

18 years agogeneration of more than one theorem per file fixed
Enrico Tassi [Sun, 14 May 2006 13:01:17 +0000 (13:01 +0000)]
generation of more than one theorem per file fixed

18 years agoadded a couple of points
Stefano Zacchiroli [Sun, 14 May 2006 06:15:39 +0000 (06:15 +0000)]
added a couple of points

18 years agotodo list about doc
Stefano Zacchiroli [Sun, 14 May 2006 04:29:40 +0000 (04:29 +0000)]
todo list about doc

18 years agomore work to produce well formed .ma files
Enrico Tassi [Sat, 13 May 2006 20:52:23 +0000 (20:52 +0000)]
more work to produce well formed .ma files

18 years agofixed some bugs
Enrico Tassi [Sat, 13 May 2006 15:12:04 +0000 (15:12 +0000)]
fixed some bugs

18 years agofull script generation
Enrico Tassi [Sat, 13 May 2006 15:11:18 +0000 (15:11 +0000)]
full script generation

18 years agofixed some pp stuff
Enrico Tassi [Sat, 13 May 2006 13:43:42 +0000 (13:43 +0000)]
fixed some pp stuff

18 years ago...
Enrico Tassi [Fri, 12 May 2006 15:25:13 +0000 (15:25 +0000)]
...

18 years agoremoved shift-reduce conflict
Enrico Tassi [Fri, 12 May 2006 15:19:40 +0000 (15:19 +0000)]
removed shift-reduce conflict

18 years agoadded parser (and future converter) of tptp files
Enrico Tassi [Fri, 12 May 2006 15:15:29 +0000 (15:15 +0000)]
added parser (and future converter) of tptp files

18 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 11 May 2006 11:27:44 +0000 (11:27 +0000)]
Bugs fixed:
 * the dependency parser no longer fails when an incomplete "include" or "set"
   are met
 * ask_and_save_moo is now performed more lazily and some bugs have been fixed

18 years agofew more bits for zack
Enrico Tassi [Tue, 9 May 2006 16:26:48 +0000 (16:26 +0000)]
few more bits for zack

18 years agohalf ported to the "new" module organization.
Enrico Tassi [Tue, 9 May 2006 13:41:00 +0000 (13:41 +0000)]
half ported to the "new" module organization.

18 years agotypes2006 patch
Enrico Tassi [Tue, 9 May 2006 13:40:24 +0000 (13:40 +0000)]
types2006 patch

18 years agoNew version of deep_subsumption
Andrea Asperti [Fri, 5 May 2006 14:56:30 +0000 (14:56 +0000)]
New version of deep_subsumption

18 years agogoal demodulated with new
Enrico Tassi [Thu, 4 May 2006 15:15:47 +0000 (15:15 +0000)]
goal demodulated with new

18 years agonew pp function for proofs
Enrico Tassi [Thu, 4 May 2006 10:55:15 +0000 (10:55 +0000)]
new pp function for proofs

18 years agoeq_chain
Enrico Tassi [Wed, 3 May 2006 11:26:21 +0000 (11:26 +0000)]
eq_chain

18 years agomore transitivity on proofs
Enrico Tassi [Wed, 3 May 2006 11:25:45 +0000 (11:25 +0000)]
more transitivity on proofs

18 years agoEquality chains.
Andrea Asperti [Thu, 27 Apr 2006 10:07:47 +0000 (10:07 +0000)]
Equality chains.
-This line, and those below, will be ignored--

M    acic_content/acic2content.ml

18 years agoAdded is_trans_eq_URI and is_sym_eq_URI
Andrea Asperti [Thu, 27 Apr 2006 10:06:54 +0000 (10:06 +0000)]
Added is_trans_eq_URI and is_sym_eq_URI

18 years agoBuild_proof_goal does not return the metasenv any more.
Andrea Asperti [Wed, 26 Apr 2006 14:53:03 +0000 (14:53 +0000)]
Build_proof_goal does not return the metasenv any more.

18 years agofixed demodulation_goal (used to return always false)
Andrea Asperti [Wed, 26 Apr 2006 13:23:55 +0000 (13:23 +0000)]
fixed demodulation_goal (used to return always false)

18 years agoremoved ocaml equality on equations
Andrea Asperti [Wed, 26 Apr 2006 13:23:29 +0000 (13:23 +0000)]
removed ocaml equality on equations

18 years agomore cleanup
Enrico Tassi [Wed, 26 Apr 2006 10:05:28 +0000 (10:05 +0000)]
more cleanup

18 years agocleanup of saturate
Enrico Tassi [Wed, 26 Apr 2006 09:59:07 +0000 (09:59 +0000)]
cleanup of saturate

18 years agoadded a new type for proofs.
Enrico Tassi [Wed, 26 Apr 2006 09:21:07 +0000 (09:21 +0000)]
added a new type for proofs.

18 years agoadded a whd (nodelta) in the carr function used by the refiner (in the eat_prods...
Enrico Tassi [Wed, 26 Apr 2006 09:16:01 +0000 (09:16 +0000)]
added a whd (nodelta) in the carr function used by the refiner (in the eat_prods case)
to get the carrier of a coercion. this is useful in case of terms generated by paramodulation
(and we want to refine the proof letting the refiner add symmetry steps)
where we have ((\lambda x:A.P(x)) t) === P'(t)
and P/P' is M=N/N=M

18 years agoBug fixed: "paste as pattern" now pastes the full pattern (e.g.
Claudio Sacerdoti Coen [Sun, 16 Apr 2006 14:45:11 +0000 (14:45 +0000)]
Bug fixed: "paste as pattern" now pastes the full pattern (e.g.
"in H:(? %)"; it used to paste "(? %)" only)

18 years agoPatch to avoid double execution of whelp queries reverted (since it seems
Claudio Sacerdoti Coen [Sat, 15 Apr 2006 16:57:24 +0000 (16:57 +0000)]
Patch to avoid double execution of whelp queries reverted (since it seems
that queries are NOT executed twice without the patch (!?!) and with the
patch the query is sometimes not executed).

18 years agouft8 string length bug fixed (Ctr-Alt-. did not work properly any longer)
Enrico Tassi [Fri, 14 Apr 2006 11:36:27 +0000 (11:36 +0000)]
uft8 string length bug fixed (Ctr-Alt-. did not work properly any longer)

18 years agomulti-instances aliases are compressed to single instances if possible
Enrico Tassi [Fri, 14 Apr 2006 10:15:48 +0000 (10:15 +0000)]
multi-instances aliases are compressed to single instances if possible