]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agoNew utility function list_index (useful in many places, I think).
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 19:28:06 +0000 (19:28 +0000)]
New utility function list_index (useful in many places, I think).

15 years agoBetter error message.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 19:12:03 +0000 (19:12 +0000)]
Better error message.

15 years agoDebug option reverted.
Claudio Sacerdoti Coen [Sat, 25 Apr 2009 18:47:14 +0000 (18:47 +0000)]
Debug option reverted.

15 years ago- matitacLib: better handling of the callbacks for the dump operation
Ferruccio Guidi [Sat, 25 Apr 2009 13:16:47 +0000 (13:16 +0000)]
- matitacLib: better handling of the callbacks for the dump operation
- applyTransformation: notation disabled when rendering reconstructed inductive types to avoid notation conflict between notation and inductive type syntax
- lexicon/lexiconEngine: better error messages and one callback removed
- termAcicContent: in lookup_interpretations, sorting the returned interpretations is optional and defaults to true (as before)
- disambiguateChoices: in lookup_symbol_by_dsc, the interpretations are not sorted before choosing, sorting them here is a bug because their order is lost so the chosen one is not the most recent
- grafiteParser: better callback functions for the drop feature of matitac, we introduced module name abbreviations for our convenience
- syntax_extensions/.depend: something is wrong with the Makefiles, this .depend is commited every time :(

15 years ago- Grammar for all obj commands ported to NG (let recs and inductives still need
Claudio Sacerdoti Coen [Fri, 24 Apr 2009 20:47:36 +0000 (20:47 +0000)]
- Grammar for all obj commands ported to NG (let recs and inductives still need
  implementation and raise assert false)
- New feature: every object can be both interactive or not, depending on the
  number of metavariables in the metasenv after disambiguation
- New objects are now put in the same namespace as old ones. The creation of
  aliases takes care of this by looking for new objects before looking for
  old ones. Note: this way the check is done twice, also when mapping
  aliases to terms. However, this is temporary code while the two "libraries"
  coexist.

15 years agoQuick&dirty implementation of neqd:
Claudio Sacerdoti Coen [Fri, 24 Apr 2009 15:11:34 +0000 (15:11 +0000)]
Quick&dirty implementation of neqd:
 a) nCicLibrary has a new function add_obj to add objects to the storage
    (that is, so far, an associative list)
 b) new command nqed
 c) GrafiteDisambiguate modified so that identifiers are resolved
    in the new storage, if possible, before going back to translating
    the old library
 d) implementation of apply_subst for terms and objects (used during nqed)
    Note: these functions are currently in nTacStatus but should be moved
    elsewhere

15 years ago- transcript: we have now two styles of mma's from grafite:
Ferruccio Guidi [Wed, 22 Apr 2009 20:47:20 +0000 (20:47 +0000)]
- transcript: we have now two styles of mma's from grafite:
  1) each includes its source (minimum choice)
  2) each includes the theory file of the source devel (maximim choice)
- matitadep: creation of the theory file is now optional and defaults to no
- procedural/library: we use style 1) above so library/theory is not needed

15 years agosyntax colouring for inverters
Wilmer Ricciotti [Wed, 22 Apr 2009 11:17:44 +0000 (11:17 +0000)]
syntax colouring for inverters

15 years agoDisabled debug prints in the inversion principle.
Wilmer Ricciotti [Wed, 22 Apr 2009 10:54:26 +0000 (10:54 +0000)]
Disabled debug prints in the inversion principle.

15 years agoNew command "inverter" used to generate an induction/inversion principle for
Wilmer Ricciotti [Wed, 22 Apr 2009 10:43:52 +0000 (10:43 +0000)]
New command "inverter" used to generate an induction/inversion principle for
inductive types. The syntax is:

  inverter name_of_the_principle for name_of_inductive_type param_selection

where param_selection is of the form

 (# # # ... #)

where # can be either ? or %. The length of param_selection must match the
number of right parameters of the inverted inductive_type. A % means that the
corresponding parameter will have an inversion hypothesis, while a ? means that
the parameter won't have an inversion hypothesis. Therefore, a selection
(??...?) will generate the traditional elimination principle, while (%%...%)
will generate a full inversion principle.

Induction/inversion principles are useful for treating inductive types such that
some of their right parameters are used uniformly in one or more constructors.
If the inverted parameters are used uniformly in some constructor, the
induction/inversion principle will provide an induction hypothesis for that
branch (while a full inversion, also ranging on non-uniform parameters, would no
provide a useful induction hypothesis).

15 years agodemodulate takes an extra argument 'all', if present it attempts to solve
Enrico Tassi [Wed, 22 Apr 2009 10:30:55 +0000 (10:30 +0000)]
demodulate takes an extra argument 'all', if present it attempts to solve
the goal demodulating it in any possible way. an extra steps argument may
be used to increase the default maximum number of demodulation steps (1).
pump may also affect the result.

15 years ago- MatitaMisc: we factorized here the function out_preamble used in matitadep
Ferruccio Guidi [Tue, 21 Apr 2009 19:49:59 +0000 (19:49 +0000)]
- MatitaMisc: we factorized here the function out_preamble used in matitadep
              and MatitacLib
- ApplyTransformation: we moved some "\n" hoping in a better rendering :)
- matitadep: we now generate a "theory" file (dfault name "theory.ma" but can
- MatitaMisc: we factorized here the function out_preamble used in matitadep
              and MatitacLib
- ApplyTransformation: we moved some "\n" hoping in a better rendering :)
- matitadep: we now generate a "theory" file (dfault name "theory.ma" but can
             be changed via the -theory cmdline option) that includes all the
     files of the devel so the devel itself can be included just
             including the theory file. To speed up the inclusion process, only
             the "top level" files are included (inclusion seems slow anyway)
- procedural/Makefile.common: new entries for single file compilation
- procedural/library: better preamble including library/theory.ma. Now the
                      devel should be reconstructed with the correct notation
- power_derivative.ma: we definitely do not want 'x' as a keyword in a serious
                       file. All files including it (for intance its
       reconstructed version) can not use 'x' as an identifier.
                       For now we replaced 'x' with 'X'
- transcript: bug fix in obtaining the list of files to be processed

15 years agofixed last file restricting auto tables
Enrico Tassi [Tue, 21 Apr 2009 13:03:55 +0000 (13:03 +0000)]
fixed last file restricting auto tables

15 years ago- init_cache_and_tables rewritten using the automation_cache
Enrico Tassi [Mon, 20 Apr 2009 07:58:14 +0000 (07:58 +0000)]
- init_cache_and_tables rewritten using the automation_cache
- new moo command Select to index an equality
- new command pump to perform some given clause steps on the automation
  cache tables
- no more imperative maxmeta in paramodulation:
  - paramodulation/* forlds a bag containing it
  - auto.ml folds tables, containing a bag

15 years agoBug fixed: variable capture in previous commit prevented all aliases insertion.
Claudio Sacerdoti Coen [Mon, 20 Apr 2009 02:26:10 +0000 (02:26 +0000)]
Bug fixed: variable capture in previous commit prevented all aliases insertion.

15 years agoSome improvements.
Claudio Sacerdoti Coen [Fri, 17 Apr 2009 12:59:20 +0000 (12:59 +0000)]
Some improvements.

15 years ago...
Claudio Sacerdoti Coen [Fri, 17 Apr 2009 12:21:54 +0000 (12:21 +0000)]
...

15 years agoProcedural: we corrected two errors about the handling of mutcase (the "cases"
Ferruccio Guidi [Thu, 16 Apr 2009 21:50:52 +0000 (21:50 +0000)]
Procedural: we corrected two errors about the handling of mutcase (the "cases"
            tactic is now disabled because it does not work well with the
    current kernel)
transcript: we immplemented uri substitution in Verbatim items
matitaInit: new option -no-default-includes for omitting the devels included by             default (this is to compile procedural/library :) )
procedural/library: bug fix

15 years agoBug: let-ins are always automatically folded!
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 15:31:10 +0000 (15:31 +0000)]
Bug: let-ins are always automatically folded!

15 years ago...
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 15:28:37 +0000 (15:28 +0000)]
...

15 years agotest/a.ma => tests/ng_tactics.ma, with nassert here and there
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 14:00:41 +0000 (14:00 +0000)]
test/a.ma => tests/ng_tactics.ma, with nassert here and there

15 years agoReplaced long, bugged implementation of letin-tac with two lines of code :-)
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 13:55:36 +0000 (13:55 +0000)]
Replaced long, bugged implementation of letin-tac with two lines of code :-)

15 years agoAdded ppterm.
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 13:39:54 +0000 (13:39 +0000)]
Added ppterm.

15 years agoThe context is now parsed in the reverse (right) order.
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 12:27:12 +0000 (12:27 +0000)]
The context is now parsed in the reverse (right) order.

15 years ago...
Claudio Sacerdoti Coen [Thu, 16 Apr 2009 12:23:22 +0000 (12:23 +0000)]
...

15 years agoUniverse is used only locally to tactics/
Enrico Tassi [Thu, 16 Apr 2009 09:46:57 +0000 (09:46 +0000)]
Universe is used only locally to tactics/
AutomationCache.cache is part of grafite_status and will
contain tables too

15 years agoadded an exception
Enrico Tassi [Thu, 16 Apr 2009 09:45:21 +0000 (09:45 +0000)]
added an exception

15 years ago- transcript: bugfix
Ferruccio Guidi [Wed, 15 Apr 2009 18:48:07 +0000 (18:48 +0000)]
- transcript: bugfix
- library: we removed most uri's. two still remain :(

15 years agowe rebuilt the dependences
Ferruccio Guidi [Tue, 14 Apr 2009 20:18:19 +0000 (20:18 +0000)]
we rebuilt the dependences

15 years ago- Procedural: generation of "exact" is now complete
Ferruccio Guidi [Tue, 14 Apr 2009 20:06:32 +0000 (20:06 +0000)]
- Procedural: generation of "exact" is now complete
-             relevant tactics are now counted correctly
- PrimitiveTactics: we set exact_tac = apply_tac as in NTactics
- transcript: the grafite parser is now working
              the "library" devel is parsed succesfully
- procedural/library: new devel.
                      Will contain the procedural reconstruction of "library"

15 years agoTrick: the refiner always subst-expands the outtype, so that the beta-redex
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 16:37:40 +0000 (16:37 +0000)]
Trick: the refiner always subst-expands the outtype, so that the beta-redex
that will be formed will always be reduced by substitution.

15 years agoBug fixed in two lines + 5 lines of comment.
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 16:16:59 +0000 (16:16 +0000)]
Bug fixed in two lines + 5 lines of comment.
During select, the context of the goal is changed and the conclusion
is changed too (too a ?[out_scope]). Then the changed conclusion was
relocated in the changed context, triggering a delift that in turn triggered
the unification case "something vs ?[out_of_scope]"... at the bad time!
Fixed by manually relocating the new conclusion in the new context.
Manually means opening and building again the cic_term data type, which is
ugly and sort of fragile.

15 years agoassert_tac now takes a list of sequents and also checks that the number of
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 13:36:39 +0000 (13:36 +0000)]
assert_tac now takes a list of sequents and also checks that the number of
sequents is the appropriate one.

It is the first example of a high-tactic that works also with the stack.

15 years agoNew debugging tactic nassert:
Claudio Sacerdoti Coen [Tue, 14 Apr 2009 12:44:31 +0000 (12:44 +0000)]
New debugging tactic nassert:

 nassert H1: t1 ... Hn: tn \vdash T

asserts (using OCaml's assert) that the current goal is equal (using
OCaml equality) to the one given the user. The substitution is fully
expanded just before calling OCaml equality.

15 years agoSemantic selection back again (but no semantic cut&paste yet).
Claudio Sacerdoti Coen [Sun, 12 Apr 2009 11:06:17 +0000 (11:06 +0000)]
Semantic selection back again (but no semantic cut&paste yet).

15 years agoMatch is now rendered as best as possible.
Claudio Sacerdoti Coen [Sun, 12 Apr 2009 10:56:31 +0000 (10:56 +0000)]
Match is now rendered as best as possible.

15 years agoThe sequent viewer now considers the context to render the Rels.
Claudio Sacerdoti Coen [Fri, 10 Apr 2009 13:19:11 +0000 (13:19 +0000)]
The sequent viewer now considers the context to render the Rels.

15 years ago- character: we adjusted some "autobatch" parameters
Ferruccio Guidi [Thu, 9 Apr 2009 18:59:12 +0000 (18:59 +0000)]
- character: we adjusted some "autobatch" parameters
- limits: in classes and subssets we now ensure the compatibility between the
  inhabitance predicate and the equivalence relation

15 years agoThe substitution is now taken in account when printing sequents in the
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 17:50:35 +0000 (17:50 +0000)]
The substitution is now taken in account when printing sequents in the
sequent viewer. Context is not yet taken in account.

15 years agoadded letin, still broken
Enrico Tassi [Thu, 9 Apr 2009 16:16:26 +0000 (16:16 +0000)]
added letin, still broken

15 years ago...
Enrico Tassi [Thu, 9 Apr 2009 16:16:04 +0000 (16:16 +0000)]
...

15 years agonew tactic whd implemented
Enrico Tassi [Thu, 9 Apr 2009 15:25:37 +0000 (15:25 +0000)]
new tactic whd implemented

15 years ago- change implemented in 4 lines
Enrico Tassi [Thu, 9 Apr 2009 15:05:29 +0000 (15:05 +0000)]
- change implemented in 4 lines
- select0 runs on hypothesis
- relocate honors conversion (but clearbody is not implemented)

15 years ago- generalize finished
Enrico Tassi [Thu, 9 Apr 2009 13:09:58 +0000 (13:09 +0000)]
- generalize finished
- relocate implemented in terms of delift

15 years ago?_OS1 := C[ ?_IN ]
Enrico Tassi [Thu, 9 Apr 2009 13:09:16 +0000 (13:09 +0000)]
?_OS1 := C[ ?_IN ]
?_IN := m
=======================
?[m;m]  =?=  ?_OS1

used to yield ? := Rel 2 instead of Rel 1, since the first m
was still out of scope when recursion reaches ?_IN

15 years agofixed modules order
Enrico Tassi [Thu, 9 Apr 2009 10:46:26 +0000 (10:46 +0000)]
fixed modules order

15 years agominor fixes
Enrico Tassi [Thu, 9 Apr 2009 09:47:05 +0000 (09:47 +0000)]
minor fixes

15 years ago...
Enrico Tassi [Thu, 9 Apr 2009 09:31:01 +0000 (09:31 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 09:22:01 +0000 (09:22 +0000)]
...

15 years ago+ Chain NCic.term -> content -> presentation very very roughly implemented
Claudio Sacerdoti Coen [Thu, 9 Apr 2009 09:20:41 +0000 (09:20 +0000)]
+ Chain  NCic.term -> content -> presentation very very roughly implemented
+ The sequent viewer now prints also the neq sequents

15 years agoJust to make it compile again.
Claudio Sacerdoti Coen [Wed, 8 Apr 2009 16:31:56 +0000 (16:31 +0000)]
Just to make it compile again.

15 years agogeneralized is half-implemented (still broken)
Enrico Tassi [Wed, 8 Apr 2009 14:18:33 +0000 (14:18 +0000)]
generalized is half-implemented (still broken)

15 years agoAnalizyng the inductive type of the eliminated term and
Enrico Tassi [Wed, 8 Apr 2009 13:15:49 +0000 (13:15 +0000)]
Analizyng the inductive type of the eliminated term and
the sort of the goals are performed by tactics having
a side-effect. This allows to write tactics like elim and cases
as lists of tactics blocked together.

15 years ago- nrewrite ((very?) rough implementation)
Claudio Sacerdoti Coen [Tue, 7 Apr 2009 22:23:31 +0000 (22:23 +0000)]
- nrewrite ((very?) rough implementation)

  PATTERNS DO NOT WORK (why?)

15 years ago- more progress towards generalize, but I am stuck now
Claudio Sacerdoti Coen [Tue, 7 Apr 2009 21:55:14 +0000 (21:55 +0000)]
- more progress towards generalize, but I am stuck now
- elim completed (up to saturation)

15 years ago- select_tac honors the hypotheses pattern when required to generalize them
Enrico Tassi [Tue, 7 Apr 2009 17:23:10 +0000 (17:23 +0000)]
- select_tac honors the hypotheses pattern when required to generalize them
- clear [names]
- initial generalize tac implementation

15 years agoselect honors the substitution
Enrico Tassi [Tue, 7 Apr 2009 17:21:41 +0000 (17:21 +0000)]
select honors the substitution

15 years agoNew tactic clear; new syntax # _; to introduce and immediately clear an
Claudio Sacerdoti Coen [Mon, 6 Apr 2009 20:40:43 +0000 (20:40 +0000)]
New tactic clear; new syntax # _; to introduce and immediately clear an
hypothesis.

15 years ago...
Claudio Sacerdoti Coen [Mon, 6 Apr 2009 19:59:21 +0000 (19:59 +0000)]
...

15 years agotactic cases works! delift clears tags
Enrico Tassi [Mon, 6 Apr 2009 17:03:55 +0000 (17:03 +0000)]
tactic cases works! delift clears tags

15 years agoeta-contraction was made on the wrong term
Enrico Tassi [Mon, 6 Apr 2009 15:50:28 +0000 (15:50 +0000)]
eta-contraction was made on the wrong term

15 years agounification:
Enrico Tassi [Mon, 6 Apr 2009 15:43:14 +0000 (15:43 +0000)]
unification:
 - the case

    (? args) v.s. ?(tag:OUT_SCOPE)

   is considered as a pattern-driven delifting.
 - the case ? args v.s. t is reduced to ?[args] v.s. t
 - eta-contraction reimplemented
 - beta-expand no longer used

delift:
 - handle out/in scope tag

ntactics:
 - elim sets the out_scope tag for 1 entry

15 years agobetter error message
Enrico Tassi [Mon, 6 Apr 2009 15:35:59 +0000 (15:35 +0000)]
better error message

15 years agoadded one exception
Enrico Tassi [Mon, 6 Apr 2009 15:35:27 +0000 (15:35 +0000)]
added one exception

15 years ago- external quantification removed (will be reintroduced when needed)
Ferruccio Guidi [Mon, 6 Apr 2009 14:20:51 +0000 (14:20 +0000)]
- external quantification removed (will be reintroduced when needed)
- preamble added (was missing)

15 years agolimits: reorganized and attached to nightly tests (cow compiles fully)
Ferruccio Guidi [Mon, 6 Apr 2009 12:42:56 +0000 (12:42 +0000)]
limits: reorganized and attached to nightly tests (cow compiles fully)

15 years agosnapshot
Enrico Tassi [Mon, 6 Apr 2009 09:01:59 +0000 (09:01 +0000)]
snapshot

15 years ago- Procedural: now we generate the exact tactic (in place of some apply tactics) and...
Ferruccio Guidi [Sun, 5 Apr 2009 23:38:16 +0000 (23:38 +0000)]
- Procedural: now we generate the exact tactic (in place of some apply tactics) and we do not perform conversion steps before it (1104 change tactics omitted in the lambda-delta devel)
- new target for the PREDICATIVE-TOPOLOGY devel: now is "limits"

15 years ago...
Enrico Tassi [Thu, 2 Apr 2009 14:43:52 +0000 (14:43 +0000)]
...

15 years agoNew file nTacStatus to:
Enrico Tassi [Thu, 2 Apr 2009 14:15:36 +0000 (14:15 +0000)]
New file nTacStatus to:
 1) collect type declarations and utility functions
 2) make cic_term as abstract as possible

15 years agoadded analyse_indty
Enrico Tassi [Thu, 2 Apr 2009 10:50:23 +0000 (10:50 +0000)]
added analyse_indty

15 years agoNew tactic "case1_tac" that make "intro" followed by case of the first
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 22:37:06 +0000 (22:37 +0000)]
New tactic "case1_tac" that make "intro" followed by case of the first
argument.

It is now possible to write things like:

napply t; ## [ #H | *W; #K1 #K2 ]

15 years ago...
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:58:50 +0000 (20:58 +0000)]
...

15 years ago## prefix is now used for tinycals
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:53:04 +0000 (20:53 +0000)]
## prefix is now used for tinycals

Example:  napply H; ##[ #H | #K];

15 years agoNew tactic intro. Syntax: "# n".
Claudio Sacerdoti Coen [Wed, 1 Apr 2009 20:40:51 +0000 (20:40 +0000)]
New tactic intro. Syntax: "# n".

15 years agoadded tentative elim
Enrico Tassi [Wed, 1 Apr 2009 16:41:20 +0000 (16:41 +0000)]
added tentative elim

15 years ago1) mk_meta now returns also the index of the created meta
Enrico Tassi [Wed, 1 Apr 2009 15:28:33 +0000 (15:28 +0000)]
1) mk_meta now returns also the index of the created meta
2) added datatypes for new patterns
3) added tactic nchange (using new patterns)
4) changed the type lowtac so that they no longer return the
   lists of open and closed goals, that are always computable
   in the new system
5) added some wrappers for kernel/refinement functions that
   work on statuses and terms labelled with their context
6) new implementation of select that performs subst-expansion.
   in-scope/out-scope used to mark regions selected by the pattern
7) ugly implementation of change based on re-opening of tagged
   subst entries

15 years agoremoved spurious "
Enrico Tassi [Wed, 1 Apr 2009 15:24:45 +0000 (15:24 +0000)]
removed spurious "

15 years agotentative subst-sexpand and change
Enrico Tassi [Mon, 30 Mar 2009 16:13:40 +0000 (16:13 +0000)]
tentative subst-sexpand and change

15 years ago...
Enrico Tassi [Mon, 30 Mar 2009 13:11:13 +0000 (13:11 +0000)]
...

15 years agomore comments
Enrico Tassi [Fri, 27 Mar 2009 12:12:50 +0000 (12:12 +0000)]
more comments

15 years agoexec and distribute implemented
Enrico Tassi [Fri, 27 Mar 2009 12:11:01 +0000 (12:11 +0000)]
exec and distribute implemented

15 years agonew apply almost there
Enrico Tassi [Thu, 26 Mar 2009 12:29:56 +0000 (12:29 +0000)]
new apply almost there

15 years ago...
Enrico Tassi [Thu, 26 Mar 2009 12:29:35 +0000 (12:29 +0000)]
...

15 years ago...
Enrico Tassi [Thu, 26 Mar 2009 12:29:28 +0000 (12:29 +0000)]
...

15 years agonew tactics are almost ready
Enrico Tassi [Wed, 25 Mar 2009 20:41:04 +0000 (20:41 +0000)]
new tactics are almost ready

15 years ago...
Claudio Sacerdoti Coen [Thu, 19 Mar 2009 22:01:12 +0000 (22:01 +0000)]
...

15 years agoadd Homepage field
Stefano Zacchiroli [Thu, 19 Mar 2009 10:13:36 +0000 (10:13 +0000)]
add Homepage field

15 years agoset package section to "ocaml"
Stefano Zacchiroli [Thu, 19 Mar 2009 10:10:18 +0000 (10:10 +0000)]
set package section to "ocaml"

15 years agoadd missing ${misc:Depends}, thanks lintian!
Stefano Zacchiroli [Thu, 19 Mar 2009 10:09:36 +0000 (10:09 +0000)]
add missing ${misc:Depends}, thanks lintian!

15 years agorelease to unstable
Stefano Zacchiroli [Thu, 19 Mar 2009 10:07:10 +0000 (10:07 +0000)]
release to unstable

15 years agodebian/*.in: more abstract substvars
Stefano Zacchiroli [Thu, 19 Mar 2009 10:05:15 +0000 (10:05 +0000)]
debian/*.in: more abstract substvars

15 years agodebian/rules: use ocaml.mk as a CDBS "rules" snippet
Stefano Zacchiroli [Thu, 19 Mar 2009 10:04:18 +0000 (10:04 +0000)]
debian/rules: use ocaml.mk as a CDBS "rules" snippet

15 years agorefresh build-dependencies for the transition
Stefano Zacchiroli [Thu, 19 Mar 2009 10:03:32 +0000 (10:03 +0000)]
refresh build-dependencies for the transition

15 years agoadded mactions, the three can now be collapsed to fit the screen
Enrico Tassi [Mon, 16 Mar 2009 12:55:03 +0000 (12:55 +0000)]
added mactions, the three can now be collapsed to fit the screen

15 years agoNew parameters for applyS: 10 20.
Andrea Asperti [Mon, 16 Mar 2009 12:41:36 +0000 (12:41 +0000)]
New parameters for applyS: 10 20.

15 years agoAdapted to new applyS.
Andrea Asperti [Mon, 16 Mar 2009 12:40:32 +0000 (12:40 +0000)]
Adapted to new applyS.

15 years agoAdded a property.
Andrea Asperti [Mon, 16 Mar 2009 12:39:54 +0000 (12:39 +0000)]
Added a property.

15 years agoMore details on the proof.
Claudio Sacerdoti Coen [Thu, 12 Mar 2009 09:37:27 +0000 (09:37 +0000)]
More details on the proof.

15 years agoNew algorithm based on in-place modification of the graph.
Claudio Sacerdoti Coen [Thu, 12 Mar 2009 00:08:54 +0000 (00:08 +0000)]
New algorithm based on in-place modification of the graph.
Conjecture solved in the negative:

(CMM?)+ | (MM?C)+

cCw = Cw
-Cw = MCw
cMw = CMw
-MMw = -w
-MCw = MMCw
iw = w