]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years agonew intro:
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

14 years agotrace generation with "// by _;"
Enrico Tassi [Fri, 7 May 2010 21:21:01 +0000 (21:21 +0000)]
trace generation with "// by _;"

14 years agonotation
Enrico Tassi [Fri, 7 May 2010 21:20:58 +0000 (21:20 +0000)]
notation

14 years agoremarks and applyS
Andrea Asperti [Fri, 7 May 2010 10:04:00 +0000 (10:04 +0000)]
remarks and applyS

14 years agoBug fixed: nstatus => status (to undo the changes).
Claudio Sacerdoti Coen [Thu, 6 May 2010 22:35:02 +0000 (22:35 +0000)]
Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

14 years ago...
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:52:38 +0000 (15:52 +0000)]
...

14 years agoFixing naming scheme for composite coercions.
Wilmer Ricciotti [Thu, 6 May 2010 15:50:07 +0000 (15:50 +0000)]
Fixing naming scheme for composite coercions.

14 years agoassert false could happen
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:45:35 +0000 (15:45 +0000)]
assert false could happen

14 years agoBug fixed:
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)]
Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

14 years agocoinduction is between us
Claudio Sacerdoti Coen [Wed, 5 May 2010 15:13:41 +0000 (15:13 +0000)]
coinduction is between us

14 years agoFirst tests.
Claudio Sacerdoti Coen [Wed, 5 May 2010 14:29:57 +0000 (14:29 +0000)]
First tests.

14 years ago* Fixed a couple of glitches in ndestruct
Wilmer Ricciotti [Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)]
* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

14 years agoRegular expressions.
Claudio Sacerdoti Coen [Tue, 4 May 2010 16:40:26 +0000 (16:40 +0000)]
Regular expressions.

14 years agonew dependences
Ferruccio Guidi [Wed, 21 Apr 2010 09:00:04 +0000 (09:00 +0000)]
new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoElimination of recursive inductive types leads to looping.
Andrea Asperti [Mon, 19 Apr 2010 09:47:02 +0000 (09:47 +0000)]
Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoalpha_eq instead of pervasives.compare
Andrea Asperti [Mon, 19 Apr 2010 09:44:21 +0000 (09:44 +0000)]
alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agobool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
Enrico Tassi [Thu, 15 Apr 2010 14:02:02 +0000 (14:02 +0000)]
bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 15:47:51 +0000 (15:47 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 14:06:35 +0000 (14:06 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFormal points.
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:42:14 +0000 (13:42 +0000)]
Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoSome dualization clean-up.
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:28:53 +0000 (13:28 +0000)]
Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed makefile
Enrico Tassi [Tue, 13 Apr 2010 19:56:18 +0000 (19:56 +0000)]
fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoauto destructs while introducing in the context
Enrico Tassi [Tue, 13 Apr 2010 19:55:18 +0000 (19:55 +0000)]
auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoprint nobjects (hack with Obj.magic)
Enrico Tassi [Tue, 13 Apr 2010 19:54:23 +0000 (19:54 +0000)]
print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agocatch the right exception, avoid uncaught Subst_not_found
Enrico Tassi [Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)]
catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosame heads different arity -> INCOMPARABLE
Enrico Tassi [Tue, 13 Apr 2010 19:52:58 +0000 (19:52 +0000)]
same heads different arity -> INCOMPARABLE

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosome fixes to THF parser
Enrico Tassi [Tue, 13 Apr 2010 19:52:26 +0000 (19:52 +0000)]
some fixes to THF parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed support file for TPTP
Enrico Tassi [Tue, 13 Apr 2010 19:51:39 +0000 (19:51 +0000)]
fixed support file for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothe edges must be quoted as well (not only the nodes)
Ferruccio Guidi [Sun, 11 Apr 2010 17:13:56 +0000 (17:13 +0000)]
the edges must be quoted as well (not only the nodes)

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoapply_subst_context on statuses
Andrea Asperti [Fri, 9 Apr 2010 14:04:08 +0000 (14:04 +0000)]
apply_subst_context on statuses

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Enrico Tassi [Thu, 8 Apr 2010 17:49:30 +0000 (17:49 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosupport axioms
Enrico Tassi [Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)]
support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Enrico Tassi [Thu, 8 Apr 2010 17:33:28 +0000 (17:33 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothf problems list for tptp 4.0.1
Enrico Tassi [Thu, 8 Apr 2010 17:31:03 +0000 (17:31 +0000)]
thf problems list for tptp 4.0.1

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed compiltion order of lexer/parser
Enrico Tassi [Thu, 8 Apr 2010 17:28:13 +0000 (17:28 +0000)]
fixed compiltion order of lexer/parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew code (unbranched) to compute all keys by all possible ways of reducing the term.
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:38:53 +0000 (16:38 +0000)]
New code (unbranched) to compute all keys by all possible ways of reducing the term.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew sets of.
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:37:26 +0000 (16:37 +0000)]
New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser received some care
Enrico Tassi [Thu, 8 Apr 2010 14:43:43 +0000 (14:43 +0000)]
THF parser received some care

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixing indexing (commit parziale di Claudio?)
Andrea Asperti [Thu, 8 Apr 2010 13:02:05 +0000 (13:02 +0000)]
Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser for TPTP
Enrico Tassi [Wed, 7 Apr 2010 13:34:29 +0000 (13:34 +0000)]
THF parser for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNot is now inductive.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 16:27:56 +0000 (16:27 +0000)]
Not is now inductive.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoUse the inversion!
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:53:12 +0000 (14:53 +0000)]
Use the inversion!

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoBug fixed: the current equation is not always the last hyp.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:41:09 +0000 (14:41 +0000)]
Bug fixed: the current equation is not always the last hyp.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:40:34 +0000 (14:40 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago- inversion principles are now generated also for co-inductive types
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:49:43 +0000 (13:49 +0000)]
- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMore debugging info from print_tac.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:35:12 +0000 (13:35 +0000)]
More debugging info from print_tac.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoImplicit and UserInput were printed incorrectly.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:33:55 +0000 (13:33 +0000)]
Implicit and UserInput were printed incorrectly.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoninversion
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:31:23 +0000 (13:31 +0000)]
ninversion

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoremoved boh
Andrea Asperti [Wed, 31 Mar 2010 10:29:30 +0000 (10:29 +0000)]
removed boh

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAdded test file for inversion in ng matita.
Wilmer Ricciotti [Wed, 31 Mar 2010 09:39:37 +0000 (09:39 +0000)]
Added test file for inversion in ng matita.

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTracing mechanism for auto. Interface changed to solve an ambiguity between
Andrea Asperti [Wed, 31 Mar 2010 09:07:11 +0000 (09:07 +0000)]
Tracing mechanism for auto. Interface changed to solve an ambiguity between
an ampty trace and a missing trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoGood definition found.
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 18:14:54 +0000 (18:14 +0000)]
Good definition found.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago(Co)Inductively Generated Formal Topologies (not only basic ones)
Claudio Sacerdoti Coen [Fri, 26 Mar 2010 17:27:53 +0000 (17:27 +0000)]
(Co)Inductively Generated Formal Topologies (not only basic ones)

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agopatched the definition of locate, advances in locate_add; still issues..
Matthias Puech [Thu, 25 Mar 2010 18:20:15 +0000 (18:20 +0000)]
patched the definition of locate, advances in locate_add; still issues..

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoZ.ma updated to reflect changes in the logical Not operator
Wilmer Ricciotti [Thu, 25 Mar 2010 18:00:49 +0000 (18:00 +0000)]
Z.ma updated to reflect changes in the logical Not operator

From: ricciott <ricciott@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAutomation problem
Matthias Puech [Thu, 25 Mar 2010 16:23:10 +0000 (16:23 +0000)]
Automation problem

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMore work
Andrea Asperti [Thu, 25 Mar 2010 14:22:31 +0000 (14:22 +0000)]
More work

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agocosi va (se vi pare).
Andrea Asperti [Thu, 25 Mar 2010 09:22:23 +0000 (09:22 +0000)]
cosi va (se vi pare).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Thu, 25 Mar 2010 09:12:41 +0000 (09:12 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoConflict(?).
Andrea Asperti [Thu, 25 Mar 2010 08:41:21 +0000 (08:41 +0000)]
Conflict(?).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoExtension of demod to arbtrary predicates (not just equalities).
Andrea Asperti [Thu, 25 Mar 2010 08:36:02 +0000 (08:36 +0000)]
Extension of demod to arbtrary predicates (not just equalities).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNice examples for automation (that fails).
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:56:32 +0000 (17:56 +0000)]
Nice examples for automation (that fails).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoSimplified proof after pattern fix
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:48:45 +0000 (17:48 +0000)]
Simplified proof after pattern fix

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago"Not" is no longer a definition
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:36:05 +0000 (17:36 +0000)]
"Not" is no longer a definition

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoThe precedence of ^-1 has changed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:35:24 +0000 (17:35 +0000)]
The precedence of ^-1 has changed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoEquality has one right parameter and thus it's elimination principle has two
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:33:09 +0000 (17:33 +0000)]
Equality has one right parameter and thus it's elimination principle has two
arguments to be protected by the scope, not 1. Why did I put one long ago in
place of 2? Maybe we were working on the old library where rewriting was non
dependent?

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 17:27:01 +0000 (17:27 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:35:57 +0000 (14:35 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoAxioms were not indexed.
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:33:55 +0000 (14:33 +0000)]
Axioms were not indexed.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:20:39 +0000 (14:20 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReal numbers as co-inductive streams of digits (overlapping refining intervals).
Claudio Sacerdoti Coen [Wed, 24 Mar 2010 14:19:52 +0000 (14:19 +0000)]
Real numbers as co-inductive streams of digits (overlapping refining intervals).

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoComputation of the trace.
Andrea Asperti [Wed, 24 Mar 2010 13:04:27 +0000 (13:04 +0000)]
Computation of the trace.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agotypo in a proof
Matthias Puech [Tue, 23 Mar 2010 18:24:49 +0000 (18:24 +0000)]
typo in a proof

From: puech <puech@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoOne more case.
Andrea Asperti [Tue, 23 Mar 2010 17:50:12 +0000 (17:50 +0000)]
One more case.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoReadded eqf_2.
Andrea Asperti [Tue, 23 Mar 2010 16:31:55 +0000 (16:31 +0000)]
Readded eqf_2.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosymmetric_eq -> sym_eq
Andrea Asperti [Tue, 23 Mar 2010 15:59:10 +0000 (15:59 +0000)]
symmetric_eq -> sym_eq

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoRe-proved an axiom
Andrea Asperti [Tue, 23 Mar 2010 15:52:29 +0000 (15:52 +0000)]
Re-proved an axiom

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoCommented a few lemmas (copies).
Andrea Asperti [Tue, 23 Mar 2010 15:51:56 +0000 (15:51 +0000)]
Commented a few lemmas (copies).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixed a few bugs
Andrea Asperti [Tue, 23 Mar 2010 15:48:42 +0000 (15:48 +0000)]
Fixed a few bugs

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago"flat" function (subst unfolding)
Andrea Asperti [Tue, 23 Mar 2010 15:45:06 +0000 (15:45 +0000)]
"flat" function (subst unfolding)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoKeeping only lift_aux e subst_aux (renamed to lift and subst).
Andrea Asperti [Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)]
Keeping only lift_aux e subst_aux (renamed to lift and subst).

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMoved compare in a different file.
Andrea Asperti [Tue, 23 Mar 2010 07:31:12 +0000 (07:31 +0000)]
Moved compare in a different file.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoDowngrading level of infix notations involving \sup.
Matthias Puech [Thu, 18 Mar 2010 17:44:52 +0000 (17:44 +0000)]
Downgrading level of infix notations involving \sup.

14 years agoPorting alla nuova def. di negazione
Andrea Asperti [Thu, 18 Mar 2010 11:36:56 +0000 (11:36 +0000)]
Porting alla nuova def. di negazione

14 years agoNuova versione di not.
Andrea Asperti [Thu, 18 Mar 2010 11:35:44 +0000 (11:35 +0000)]
Nuova versione di not.

14 years agoPrintings removed.
Andrea Asperti [Thu, 18 Mar 2010 11:33:10 +0000 (11:33 +0000)]
Printings removed.

14 years agoDebugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:28:46 +0000 (11:28 +0000)]
Debugging disabled.

14 years agoDebugging disabled.
Andrea Asperti [Thu, 18 Mar 2010 11:28:22 +0000 (11:28 +0000)]
Debugging disabled.

14 years agoNew demodulation tactics (mostly for debugging purposes).
Andrea Asperti [Thu, 18 Mar 2010 11:23:53 +0000 (11:23 +0000)]
New demodulation tactics (mostly for debugging purposes).
It is called with "nauto demod".

14 years agoExporting the demodulation function.
Andrea Asperti [Thu, 18 Mar 2010 11:22:11 +0000 (11:22 +0000)]
Exporting the demodulation function.

14 years agoNew option "demod" for auto.
Andrea Asperti [Thu, 18 Mar 2010 11:19:53 +0000 (11:19 +0000)]
New option "demod" for auto.

14 years agoPorting the new definition of equality.
Andrea Asperti [Thu, 18 Mar 2010 11:06:34 +0000 (11:06 +0000)]
Porting the new definition of equality.

14 years agoDo not index examples (concrete syntax: nremark).
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:46 +0000 (10:21 +0000)]
Do not index examples (concrete syntax: nremark).

14 years agonremark => `Example (not to be indexed)
Claudio Sacerdoti Coen [Thu, 18 Mar 2010 10:21:14 +0000 (10:21 +0000)]
nremark => `Example (not to be indexed)

14 years agoapp of app inside smart application.
Andrea Asperti [Thu, 18 Mar 2010 07:18:36 +0000 (07:18 +0000)]
app of app inside smart application.

14 years agodr
Ferruccio Guidi [Wed, 17 Mar 2010 15:10:12 +0000 (15:10 +0000)]
dr
brs line, and those below, will be ignored--

M    ng_tactics/.depend.opt

14 years agoqualche caso del lemma 5.2.11
Andrea Asperti [Wed, 17 Mar 2010 14:58:51 +0000 (14:58 +0000)]
qualche caso del lemma 5.2.11

14 years agoOCaml's inferred type simplified.
Claudio Sacerdoti Coen [Wed, 17 Mar 2010 14:56:31 +0000 (14:56 +0000)]
OCaml's inferred type simplified.

14 years ago...
Claudio Sacerdoti Coen [Wed, 17 Mar 2010 14:29:27 +0000 (14:29 +0000)]
...

14 years agoSplitted gpts in two files.
Andrea Asperti [Wed, 17 Mar 2010 11:51:01 +0000 (11:51 +0000)]
Splitted gpts in two files.