]> matita.cs.unibo.it Git - helm.git/log
helm.git
17 years agopreliminary cookie support
Stefano Zacchiroli [Mon, 29 Jan 2007 10:43:50 +0000 (10:43 +0000)]
preliminary cookie support

17 years agoAdded option datatype. Required (for technicalities/Setoids.ma).
Claudio Sacerdoti Coen [Sat, 27 Jan 2007 16:32:56 +0000 (16:32 +0000)]
Added option datatype. Required (for technicalities/Setoids.ma).

17 years ago"Warning/error/debug/infos" messages now sent on stderr.
Claudio Sacerdoti Coen [Fri, 26 Jan 2007 13:15:56 +0000 (13:15 +0000)]
"Warning/error/debug/infos" messages now sent on stderr.

17 years agoSome changes:
Claudio Sacerdoti Coen [Fri, 26 Jan 2007 13:04:44 +0000 (13:04 +0000)]
Some changes:
1. error messages are now in HTML (they used to be in plain text + vt100 colour
   scheme)
2. commands are now expected to be in a fragment of the pgip protocol.
   Supported commands are:
    <pgip><doitem>...</doitem></pgip>
    <pgip><undoitem>...</undoitem></pgip>
3. the terminator sent back is now preceded by either -1 (command not
   successful) or n (an integer to be sent for undoing)
4. undoing is now supported

17 years agotactics.mli: regenerated
Ferruccio Guidi [Wed, 24 Jan 2007 19:44:22 +0000 (19:44 +0000)]
tactics.mli: regenerated
LambdaDelta: regenerated with some new theorems

17 years agomatitaGui: some missing cases during disambiguation now treated
Ferruccio Guidi [Wed, 24 Jan 2007 19:28:15 +0000 (19:28 +0000)]
matitaGui: some missing cases during disambiguation now treated
grafiteAst: rename tactic removed
procedural: some improvements

17 years agosend internally generated headers in lowercase form for consistency
Stefano Zacchiroli [Wed, 24 Jan 2007 09:10:03 +0000 (09:10 +0000)]
send internally generated headers in lowercase form for consistency

17 years agosome patches
Ferruccio Guidi [Mon, 22 Jan 2007 18:12:54 +0000 (18:12 +0000)]
some patches

17 years agoJust a few lines test to understand with Cezary Kalinsky how much effort is
Claudio Sacerdoti Coen [Sat, 20 Jan 2007 16:20:16 +0000 (16:20 +0000)]
Just a few lines test to understand with Cezary Kalinsky how much effort is
required to integrate Matita in his generic AJAX based interface.
matitawiki is an executable that reads from stdin and prints output and error on
stdout/stderr (both followed by (Char.chr 249) after each command).
All the interactive commands (thus also "undo") are not supported.

17 years agoBug fixed: if the context of a sequent was empty a vertical box without content
Claudio Sacerdoti Coen [Sat, 20 Jan 2007 15:31:18 +0000 (15:31 +0000)]
Bug fixed: if the context of a sequent was empty a vertical box without content
was generated. This is not allowed by BoxPp (assert failure).

17 years agoAdded new function txt_of_cic_sequent.
Claudio Sacerdoti Coen [Sat, 20 Jan 2007 15:30:26 +0000 (15:30 +0000)]
Added new function txt_of_cic_sequent.

17 years ago1. buf fixed in eval_from_stream when first_statemente_only=true:
Claudio Sacerdoti Coen [Sat, 20 Jan 2007 15:29:51 +0000 (15:29 +0000)]
1. buf fixed in eval_from_stream when first_statemente_only=true:
   the last computed states were lost
2. added a new watcher function to eval_from_stream.
   The function is called after the execution of each command.

17 years agoAn "assert false" used to be raised when matitac was started on an empty file.
Claudio Sacerdoti Coen [Sat, 20 Jan 2007 15:16:55 +0000 (15:16 +0000)]
An "assert false" used to be raised when matitac was started on an empty file.

17 years agosome updates
Ferruccio Guidi [Fri, 19 Jan 2007 14:30:00 +0000 (14:30 +0000)]
some updates

17 years agoUnified: refactoring
Ferruccio Guidi [Fri, 19 Jan 2007 14:20:38 +0000 (14:20 +0000)]
Unified: refactoring

17 years agoUnified: refactoring
Ferruccio Guidi [Thu, 18 Jan 2007 21:55:14 +0000 (21:55 +0000)]
Unified: refactoring

17 years agoUnified refactoring
Ferruccio Guidi [Thu, 18 Jan 2007 15:08:29 +0000 (15:08 +0000)]
Unified refactoring

17 years agoUnified: refactoring
Ferruccio Guidi [Thu, 18 Jan 2007 14:49:03 +0000 (14:49 +0000)]
Unified: refactoring

17 years agonew version, using new tacticals
Wilmer Ricciotti [Thu, 18 Jan 2007 11:51:05 +0000 (11:51 +0000)]
new version, using new tacticals

17 years agoThis is the roadmap of the constructive proof of Lebesgue's dominated
Enrico Zoli [Wed, 17 Jan 2007 17:59:59 +0000 (17:59 +0000)]
This is the roadmap of the constructive proof of Lebesgue's dominated
convergence theorem in the order theoretic setting. I.e. we speak of
convergence (in terms of liminf and limsup) and not of norms/measures.

The formulation should be fully constructive:
 1. the exceeds relation is used in place of the derived negative notion
    <= for partial orders
 2. strong sup and infs are used in place of the weaker sup and infs
 3. the statement of Lebesgue's dominated converge theorem is just
    extensionality of the functional
      \lambda f. liminf f a_n
    with respect to the apartness relation # over real numbers and the
    exceeds/apartness relation over partial orders.

Interesting points to be noticed:
 a) one lemma used in the proof is Fatou. This lemma can be given in the
    usual negative formulation (i.e. on <=)
 b) another lemma used in the proof is that the liminf is less or equal to
    the limsup. This lemm can be given in the usual negative formulation
    (i.e. on <=). Moreover, we feel that if <= is not defined as
    ~< it is actually impossible to constructively prove it.

17 years agoCoRN (new version) has been committed by Andrea in library/algebra/CoRN.
Claudio Sacerdoti Coen [Wed, 17 Jan 2007 15:36:48 +0000 (15:36 +0000)]
CoRN (new version) has been committed by Andrea in library/algebra/CoRN.

17 years agoAdded SetoidInc.m
Andrea Asperti [Tue, 16 Jan 2007 12:18:09 +0000 (12:18 +0000)]
Added SetoidInc.m

17 years agoSome CoRN files.
Andrea Asperti [Tue, 16 Jan 2007 12:08:31 +0000 (12:08 +0000)]
Some CoRN files.

17 years agoprocedural: added fwd rewrite in arbitrary proofs (not just premises)
Ferruccio Guidi [Fri, 12 Jan 2007 19:34:58 +0000 (19:34 +0000)]
procedural: added fwd rewrite in arbitrary proofs (not just premises)
            added whd conversion before intros when needed
prova.ma  : highlighted a bug with the "in" clause of the "match" constr.

17 years agoprocedural: buggy ast renderer fixed
Ferruccio Guidi [Wed, 10 Jan 2007 19:36:37 +0000 (19:36 +0000)]
procedural: buggy ast renderer fixed

17 years agoattributes now in the proof status: commit 4
Ferruccio Guidi [Wed, 10 Jan 2007 17:14:52 +0000 (17:14 +0000)]
attributes now in the proof status: commit 4

17 years agoattributes now in the proof status: commit 3
Ferruccio Guidi [Wed, 10 Jan 2007 14:30:22 +0000 (14:30 +0000)]
attributes now in the proof status: commit 3

17 years agoattributes now in the proof status: commit 2
Ferruccio Guidi [Wed, 10 Jan 2007 14:27:27 +0000 (14:27 +0000)]
attributes now in the proof status: commit 2

17 years agoattributes now in the proof status: commit 1
Ferruccio Guidi [Wed, 10 Jan 2007 14:23:47 +0000 (14:23 +0000)]
attributes now in the proof status: commit 1

17 years agoPorting of setoids.ma from Coq continued.
Claudio Sacerdoti Coen [Sun, 7 Jan 2007 18:32:18 +0000 (18:32 +0000)]
Porting of setoids.ma from Coq continued.
The fact that simplification does not work properly slows down the whole
process.

17 years agoBug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
Claudio Sacerdoti Coen [Sun, 7 Jan 2007 18:17:56 +0000 (18:17 +0000)]
Bug fixed in definition of cic:/.../setoids/make_compatibility_goal_aux.con:
two generalizes were done in the wrong order, permuting the arguments and
making every relation change its variance!

17 years ago- inside dicrimination_tree is now checked the invariant that bad terms are indexed...
Enrico Tassi [Sat, 6 Jan 2007 16:16:40 +0000 (16:16 +0000)]
- inside dicrimination_tree is now checked the invariant that bad terms are indexed, but this invariant is not always respected, so a 'Dead' representative is used and a warning is printed.
- autoCache (should) not index bad terms

17 years ago;auto fixed
Enrico Tassi [Sat, 6 Jan 2007 16:14:06 +0000 (16:14 +0000)]
;auto fixed

17 years agoremoved debugging printing
Enrico Tassi [Fri, 5 Jan 2007 11:40:13 +0000 (11:40 +0000)]
removed debugging printing

17 years agodebuggin message improved
Enrico Tassi [Fri, 5 Jan 2007 11:37:47 +0000 (11:37 +0000)]
debuggin message improved

17 years agoadd_moo_content does not add a coercion statement twice
Enrico Tassi [Fri, 5 Jan 2007 11:37:25 +0000 (11:37 +0000)]
add_moo_content does not add a coercion statement twice

17 years agoAdded check for duplicate (convertible) composite coercions,
Enrico Tassi [Fri, 5 Jan 2007 11:36:41 +0000 (11:36 +0000)]
Added check for duplicate (convertible) composite coercions,
that are not added anymore.
Nicer api for meets used by unification.

17 years agoErroneously declared coercion removed
Enrico Tassi [Fri, 5 Jan 2007 11:07:04 +0000 (11:07 +0000)]
Erroneously declared coercion removed

17 years agoready for ocamlnet 2.2
Stefano Zacchiroli [Wed, 3 Jan 2007 19:16:56 +0000 (19:16 +0000)]
ready for ocamlnet 2.2

17 years agomore elegant handling of all/opt building
Stefano Zacchiroli [Wed, 3 Jan 2007 19:16:49 +0000 (19:16 +0000)]
more elegant handling of all/opt building

17 years agoNotation is finally fully working everywhere.
Claudio Sacerdoti Coen [Wed, 3 Jan 2007 17:33:22 +0000 (17:33 +0000)]
Notation is finally fully working everywhere.
What a great day!

17 years agoDebugging code removed.
Claudio Sacerdoti Coen [Wed, 3 Jan 2007 17:09:32 +0000 (17:09 +0000)]
Debugging code removed.

17 years agoRiesz_spaces are now seen as lattices + vector spaces + ordered abelian groups.
Claudio Sacerdoti Coen [Wed, 3 Jan 2007 14:49:18 +0000 (14:49 +0000)]
Riesz_spaces are now seen as lattices + vector spaces + ordered abelian groups.

17 years agooder tests
Enrico Tassi [Wed, 3 Jan 2007 09:24:11 +0000 (09:24 +0000)]
oder tests

17 years agoThere used to be two minimal joins between an ordered_set and an abelian_group:
Claudio Sacerdoti Coen [Tue, 2 Jan 2007 20:05:21 +0000 (20:05 +0000)]
There used to be two minimal joins between an ordered_set and an abelian_group:
ordered_field_ch0 and riesz_space. To avoid the problem without introducing
backtracking in unification I have introduced ordered_abelian_groups.
An ordered_field_ch0 is recast as a field that is also an ordered_abelian_group
and a cotransitively_ordered_set. I still have to recast riesz_spaces as
vector spaces that are also ordered_abelian_groups and lattices.

17 years agoSame fix of the previous commit, but in a different case.
Claudio Sacerdoti Coen [Tue, 2 Jan 2007 19:03:33 +0000 (19:03 +0000)]
Same fix of the previous commit, but in a different case.

17 years ago1. More debugging code
Claudio Sacerdoti Coen [Tue, 2 Jan 2007 19:00:34 +0000 (19:00 +0000)]
1. More debugging code
2. "Bug" "fixed": when the pullback of two coercions is computed, only the
   join is returned, but not the two coercions that complete the pullback.
   Thus we need to recompute them and it may happen that we find more than one
   parallel coercions. This "fix" just randomly picks the first one (instead
   of raising an assert false). All this stuff must be handled in a better way.

17 years agoadded oblivion_universe and used it in paxck_coercions
Enrico Tassi [Tue, 2 Jan 2007 18:03:59 +0000 (18:03 +0000)]
added oblivion_universe and used it in paxck_coercions

17 years agosome tests patched
Ferruccio Guidi [Sun, 31 Dec 2006 14:49:11 +0000 (14:49 +0000)]
some tests patched

17 years agoSome more notation can now be used.
Claudio Sacerdoti Coen [Sat, 30 Dec 2006 21:20:26 +0000 (21:20 +0000)]
Some more notation can now be used.
However, in integration_algebras.ma there are several situations where
multiple meets are found and notation cannot be used.

17 years agole x y ==> x \leq y (now possible because of a bug fix in coercion
Claudio Sacerdoti Coen [Sat, 30 Dec 2006 21:00:18 +0000 (21:00 +0000)]
le x y ==> x \leq y  (now possible because of a bug fix in coercion
serialization in .moo files)

17 years agoSerious bug fixed: arities of coercions in the .moo files were not computed
Claudio Sacerdoti Coen [Sat, 30 Dec 2006 20:56:13 +0000 (20:56 +0000)]
Serious bug fixed: arities of coercions in the .moo files were not computed
correctly. Thus including another file a bugged coercion graph was produced,
with randomic effects quite hard to understand. (Examples in dama where
it was not possible to use <= in place of le here and there because of a
coercion with the wrong arity).

17 years ago dependence to legacy/coq.ma fixed
Ferruccio Guidi [Sat, 30 Dec 2006 18:59:14 +0000 (18:59 +0000)]
 dependence to legacy/coq.ma fixed

17 years agonow we try two distinct depend files for compilation in byte and native code
Ferruccio Guidi [Fri, 29 Dec 2006 14:35:31 +0000 (14:35 +0000)]
now we try two distinct depend files for compilation in byte and native code

17 years agoRecord with simulated manifest types are now used everywhere in
Claudio Sacerdoti Coen [Fri, 29 Dec 2006 14:35:28 +0000 (14:35 +0000)]
Record with simulated manifest types are now used everywhere in
integration_algebras.ma. They seem to work really very well (up to missing
but due syntactic sugar).

17 years agoFirst attempt at using/simulating records with manifest types to encode
Claudio Sacerdoti Coen [Fri, 29 Dec 2006 14:08:44 +0000 (14:08 +0000)]
First attempt at using/simulating records with manifest types to encode
mathematical structures that form a DAG. So far it works quite well,
but the generation of the "coerced" projection should be automated.
Something to write a paper on.

17 years agoeq_ind' generalized to eq_rect'
Claudio Sacerdoti Coen [Fri, 29 Dec 2006 14:05:25 +0000 (14:05 +0000)]
eq_ind' generalized to eq_rect'

17 years ago- tactics:
Ferruccio Guidi [Fri, 29 Dec 2006 11:28:13 +0000 (11:28 +0000)]
- tactics:
  rename tactic enabled,
  rewrite and rewrite_simpl now take optional names for the rewrited premises
- procedural script reconstruction
  now starts directly from acic bypassing the content level,
  the script for the use case proof in matita/contribs/prova.ma is reconstructed  completely now and is correctly parsed and typechecked

17 years agoYet another localization error in eat_prods fixed.
Claudio Sacerdoti Coen [Thu, 28 Dec 2006 17:12:06 +0000 (17:12 +0000)]
Yet another localization error in eat_prods fixed.
However, the fix is very very ugly (it uses unsharing) and clearly shows
a source of inefficiency (and possibly also divergence, I would say).

17 years ago.depends committed to fix non-compilation errors
Claudio Sacerdoti Coen [Thu, 28 Dec 2006 14:59:27 +0000 (14:59 +0000)]
.depends committed to fix non-compilation errors

17 years agosome depend files
Ferruccio Guidi [Sun, 24 Dec 2006 15:02:39 +0000 (15:02 +0000)]
some depend files

17 years agolegacy development created
Ferruccio Guidi [Fri, 22 Dec 2006 16:32:46 +0000 (16:32 +0000)]
legacy development created

17 years ago- sc3/props.ma sc3/arity.ma: dependences fixed
Ferruccio Guidi [Fri, 22 Dec 2006 14:54:38 +0000 (14:54 +0000)]
- sc3/props.ma sc3/arity.ma: dependences fixed
- csubc/arity.ma csubc/csuba.ma: reverted as no fix was needed

17 years agoAdd_moo_content modified to avoid repetitions of index command during inclusion.
Andrea Asperti [Fri, 22 Dec 2006 10:53:52 +0000 (10:53 +0000)]
Add_moo_content modified to avoid repetitions of index command during inclusion.

17 years agoMinor change.
Andrea Asperti [Fri, 22 Dec 2006 10:51:43 +0000 (10:51 +0000)]
Minor change.

17 years agoCollapse_head_metas transforms all terms "not-recongnized" into a
Andrea Asperti [Fri, 22 Dec 2006 10:43:54 +0000 (10:43 +0000)]
Collapse_head_metas transforms all terms "not-recongnized" into a
meta.

17 years agoIn the let-in case we compute the type and add it to the context.
Andrea Asperti [Fri, 22 Dec 2006 10:37:35 +0000 (10:37 +0000)]
In the let-in case we compute the type and add it to the context.
Before it was computed every time

17 years agoThe function uri_of_term now works also if the explciit substitution list
Andrea Asperti [Fri, 22 Dec 2006 10:30:59 +0000 (10:30 +0000)]
The function uri_of_term now works also if the explciit substitution list
is not empty.

17 years agoSpeeedup! (by caching)
Enrico Tassi [Fri, 22 Dec 2006 08:54:57 +0000 (08:54 +0000)]
Speeedup! (by caching)
The costing operation is baseuri_of_file that parses the whole maybe big file to extract the first command line.

17 years agoadded some missing includes
Enrico Tassi [Thu, 21 Dec 2006 16:37:06 +0000 (16:37 +0000)]
added some missing includes

17 years agoNew declarative tactic "we proceed by cases on t to prove t'".
Claudio Sacerdoti Coen [Wed, 20 Dec 2006 23:25:42 +0000 (23:25 +0000)]
New declarative tactic "we proceed by cases on t to prove t'".
Very unsatisfactory since it already introduces the hypothesis in advance,
actually ignoring the following "case S (n:nat)" declarative command.
I do not see any easy solution at all.

17 years agoBug fixed in cases (it did not produced the right number of lambdas for the
Claudio Sacerdoti Coen [Wed, 20 Dec 2006 23:23:41 +0000 (23:23 +0000)]
Bug fixed in cases (it did not produced the right number of lambdas for the
outtype of dependent inductive types).

17 years agoTactic cases documented
Claudio Sacerdoti Coen [Wed, 20 Dec 2006 22:39:19 +0000 (22:39 +0000)]
Tactic cases documented

17 years agoNew tactic cases (still to be documented).
Claudio Sacerdoti Coen [Wed, 20 Dec 2006 22:34:35 +0000 (22:34 +0000)]
New tactic cases (still to be documented).
It is necessary for the declarative language and it is useful anyway.

17 years agoProcedural: method "Apply" ok in forward style
Ferruccio Guidi [Wed, 20 Dec 2006 20:07:54 +0000 (20:07 +0000)]
Procedural: method "Apply" ok in forward style

17 years agoProcedural: "ByInduction" method ok
Ferruccio Guidi [Tue, 19 Dec 2006 19:21:36 +0000 (19:21 +0000)]
Procedural:   "ByInduction" method ok
GrafiteAstPp: letin tactic now works

17 years agoAn idea to implement manifest record fields:
Claudio Sacerdoti Coen [Mon, 18 Dec 2006 22:28:22 +0000 (22:28 +0000)]
An idea to implement manifest record fields:
record r : R := { c1 : T1 ; c2 : T2 with f c1 = g c2 }.

Only the syntactic sugar is actually missing!

17 years agoProcedural: some improvements
Ferruccio Guidi [Mon, 18 Dec 2006 21:10:52 +0000 (21:10 +0000)]
Procedural: some improvements

17 years agoM logic/coimplication.ma
Andrea Asperti [Mon, 18 Dec 2006 12:01:11 +0000 (12:01 +0000)]
M    logic/coimplication.ma

17 years agoRenamed iterative into map_iter_p and moved around a few theorems.
Andrea Asperti [Mon, 18 Dec 2006 11:52:57 +0000 (11:52 +0000)]
Renamed iterative into map_iter_p and moved around a few theorems.

17 years agoProof of Euler theorem.
Andrea Asperti [Mon, 18 Dec 2006 10:09:01 +0000 (10:09 +0000)]
Proof of Euler theorem.

17 years agoUp to definition of limsup as liminf computed on the reverse ordering.
Enrico Zoli [Fri, 15 Dec 2006 18:59:00 +0000 (18:59 +0000)]
Up to definition of limsup as liminf computed on the reverse ordering.
However, I am no longer sure that this is the best way to proceed since
the lemmas to be proved are a lot and the typing is difficult. However,
this work should be done anyway to state limsup f x = - liminf f (-x)
that we need anyway.

17 years agoFatou lemma achieved (up to a few more axioms here and there...)
Enrico Zoli [Fri, 15 Dec 2006 16:11:56 +0000 (16:11 +0000)]
Fatou lemma achieved (up to a few more axioms here and there...)

17 years agoHuge DAMA update:
Claudio Sacerdoti Coen [Fri, 15 Dec 2006 10:39:07 +0000 (10:39 +0000)]
Huge DAMA update:
 1. up to Fatou lemma (almost there)
 2. requires the new unification procedure for coercions to enable
    multiple coercion paths between two nodes
 3. it stresses CicUniv.mere_ugraphs. To compile the new DAMA file quickly
    you have to disable that function :-(

17 years agoBugged code patched, but not in the optimal way.
Claudio Sacerdoti Coen [Thu, 14 Dec 2006 18:50:09 +0000 (18:50 +0000)]
Bugged code patched, but not in the optimal way.
The problem is that in two different interpretations a symbol id can be
interpreted as dsc in different locations. Using the previous code it
happened that every interpretation was pruned out since a symbol id occurred
twice (in different locations) in an/every interpretation. Now the couples
(loc,id) are considered for disambiguating between the two interpretations.
However, this way we hide information to the user (what other occurrences of
the same symbol are given the same interpretation).

17 years agoDebugging code commented out.
Claudio Sacerdoti Coen [Thu, 14 Dec 2006 18:48:00 +0000 (18:48 +0000)]
Debugging code commented out.

17 years ago...
Enrico Tassi [Thu, 14 Dec 2006 18:15:55 +0000 (18:15 +0000)]
...

17 years ago...
Enrico Tassi [Thu, 14 Dec 2006 18:15:39 +0000 (18:15 +0000)]
...

17 years ago...
Enrico Tassi [Thu, 14 Dec 2006 18:14:07 +0000 (18:14 +0000)]
...

17 years agocontent2Procedural.ml: "Intros+LetTac" ok
Ferruccio Guidi [Thu, 14 Dec 2006 15:38:40 +0000 (15:38 +0000)]
content2Procedural.ml: "Intros+LetTac" ok

17 years agoHuge commit:
Claudio Sacerdoti Coen [Thu, 14 Dec 2006 13:41:38 +0000 (13:41 +0000)]
Huge commit:

 1. coercGraph.ml* moved from library to cic_unification (where it should
    have been put in the first place). A few functions that must remain in
   library moved to coercDb.ml* (where they should have been put in the first
   place)
 2. ProofEngineHelpers.saturate_term moved from tactic to cic_unification.
 3. Bug fixed in saturate_term: the newmeta returned by the function was not
    correct in some cases
 4. CoercGraph.look_for_coercion* used to saturate the coercion with implicit
    arguments (thus requirin a refinement pass later on). Now the same
    functions saturate the term with metas. The return type has changed
    accordingly.
 5. the horrible hack to break composite coercions during unification has been
    replaced by a nice implementation of unification towards the join of the
    two coercions (called meet by Enrico I do not know why :-).
    This solves many many problems found using multiple coercion pathes from
    a source to a destination. (This is the case in DAMA that I am going to
    commit soon).

17 years ago- transcript: patched to generate aliases instead of inlined variables
Ferruccio Guidi [Wed, 13 Dec 2006 19:50:03 +0000 (19:50 +0000)]
- transcript: patched to generate aliases instead of inlined variables
- CoRN-Decl: regenerated with aliases instead of inlined variables
- content2Procedural: improved but not working yet

17 years agowe parametrized CicNotationPt.obj on 'term
Ferruccio Guidi [Tue, 12 Dec 2006 14:04:59 +0000 (14:04 +0000)]
we parametrized CicNotationPt.obj on 'term

17 years agowe started the infrastructure for the procedural rendering of proofs
Ferruccio Guidi [Tue, 12 Dec 2006 09:54:14 +0000 (09:54 +0000)]
we started the infrastructure for the procedural rendering of proofs

17 years agowe exported some inversors from coq
Ferruccio Guidi [Sat, 9 Dec 2006 16:21:32 +0000 (16:21 +0000)]
we exported some inversors from coq

17 years agoEXPERIMENTAL:
Claudio Sacerdoti Coen [Fri, 8 Dec 2006 17:36:24 +0000 (17:36 +0000)]
EXPERIMENTAL:
 1. the disambiguation domain is now a tree that partially reflects the
    applicative structure of the term
 2. disambiguation now classifies errors according to the following criterium:
    an error E is considered not significant when it belongs to the set A of
    results (obtained interpreting a symbol and its subterms in every possible
    way) and there exists at least a result in A that is either OK or Uncertain.
    A "subterm" is implicitly defined by the tree structure of the
    disambiguation domain.
 3. WARNING: there used to be an (important ????) optimization that has not
    been ported (yet ???): if the next item in the disambiguation domain can
    be interpreted in just one way, we skip the current refinement step.
    According to tests on my laptop the optimization does not seem to be
    really so significant (sometimes it even slow down???). We will decide
    on monday whether porting it or not. Porting it is not very simple because
    of the new data structures involved.

17 years agoDisambiguation errors in phase 3 that are not present in phase 4 are filtered
Claudio Sacerdoti Coen [Fri, 8 Dec 2006 11:39:07 +0000 (11:39 +0000)]
Disambiguation errors in phase 3 that are not present in phase 4 are filtered
out. Explanation: if they are only in phase 3, it means that in phase 4 they
are not significative. Thus we conclude that phase 3 is not significative.
There is a drawback: equality over errors is not very well defined because
of Metas in error messages. Thus it could be the case that we remove the error
in phase 3 when the same error is still there in phase 4.

17 years agonew makefiles
Ferruccio Guidi [Fri, 8 Dec 2006 09:50:02 +0000 (09:50 +0000)]
new makefiles

17 years agoreverted error committed by mistake
Stefano Zacchiroli [Thu, 7 Dec 2006 18:20:52 +0000 (18:20 +0000)]
reverted error committed by mistake

17 years agoavoid Failure "nth" when only one disambiguation pass is enabled
Stefano Zacchiroli [Thu, 7 Dec 2006 18:19:57 +0000 (18:19 +0000)]
avoid Failure "nth" when only one disambiguation pass is enabled