]> matita.cs.unibo.it Git - helm.git/log
helm.git
15 years agoEXPERIMENTAL COMMIT (part B, by CSC :-):
Enrico Tassi [Mon, 15 Jun 2009 16:41:47 +0000 (16:41 +0000)]
EXPERIMENTAL COMMIT (part B, by CSC :-):
 - objects are now individually serialized too
   (but never decompiled)

CRITICAL OBSERVATION:
 - closures in ocaml are pointers in the binary, hence the library
   must be decompiled at every single change in matita's code

15 years agoEXPERIMENTAL COMMIT (by CSC,actuall :-)
Enrico Tassi [Mon, 15 Jun 2009 16:22:18 +0000 (16:22 +0000)]
EXPERIMENTAL COMMIT (by CSC,actuall :-)
This commit partially implements (in NCicLibrary) serialization for NG.
It creates several .matita/matita/.../foo.ng files that are ocaml dumps
of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied
to the current status.

The test tests/ng_includeB.ma shows how unification hints are preserved.

TODO:
 a) decompilation is implemented in NCicLibrary, but not called anywhere
 b) serialization of objects (and "query" db (and old to new cache??)) not
    implemented yet
 c) objects are removed from the library, but not from the environment!

15 years ago...
Enrico Tassi [Mon, 15 Jun 2009 11:18:02 +0000 (11:18 +0000)]
...

15 years agoadded TODO list
Enrico Tassi [Mon, 15 Jun 2009 11:14:48 +0000 (11:14 +0000)]
added TODO list

15 years agohuge commit regarding the grafite_status:
Enrico Tassi [Mon, 15 Jun 2009 11:04:24 +0000 (11:04 +0000)]
huge commit regarding the grafite_status:
- in the ng_status component it embeds the lexicon status
- the lexicon status is not passed around alone anymore
- coercions/hints for the ng system are no longer imperative
  (are in the e (for external) status of the tac_status
- ng_refiner does not take in input a look_for_coercions function
  but an aggregate type "rdb" comprising hints and coercions
  (and empty one is passed to disable hints/coercions)
functionalities losses:
- old (generated) hint are no longer translated on the fly
- old coercions are translated in a best effort way
  (no universes calculation)

15 years agopart of last commit
Enrico Tassi [Mon, 15 Jun 2009 09:41:44 +0000 (09:41 +0000)]
part of last commit

15 years agotacticals are really tactics now, they have an AST at the same level of
Enrico Tassi [Mon, 15 Jun 2009 09:36:46 +0000 (09:36 +0000)]
tacticals are really tactics now, they have an AST at the same level of
tactics. Parser/engine fixed accordingly. This allowed a better TPTP
exportation

15 years agowe removed some coercion detours and we added some coercions we really would like...
Ferruccio Guidi [Sat, 13 Jun 2009 19:00:52 +0000 (19:00 +0000)]
we removed some coercion detours and we added some coercions we really would like to see

15 years agoImplemented keep_simplified.
denes [Fri, 12 Jun 2009 16:16:11 +0000 (16:16 +0000)]
Implemented keep_simplified.
If a candidate for forward inference is discarded, another is selected

15 years agoocaml sucks...
Claudio Sacerdoti Coen [Fri, 12 Jun 2009 13:46:40 +0000 (13:46 +0000)]
ocaml sucks...

15 years ago...
Claudio Sacerdoti Coen [Fri, 12 Jun 2009 13:07:00 +0000 (13:07 +0000)]
...

15 years ago-ng implemented
Enrico Tassi [Fri, 12 Jun 2009 13:04:13 +0000 (13:04 +0000)]
-ng implemented

15 years agoAdded a new keep_simplified function
Andrea Asperti [Fri, 12 Jun 2009 12:33:45 +0000 (12:33 +0000)]
Added a new keep_simplified function

15 years agoRenamed forward_simplify into simplify and backward_simplify
Andrea Asperti [Fri, 12 Jun 2009 11:21:13 +0000 (11:21 +0000)]
Renamed forward_simplify into simplify and backward_simplify
into simplify_goal

15 years agoActive goals are now demodulated after selecting a positive clause.
denes [Thu, 11 Jun 2009 22:52:38 +0000 (22:52 +0000)]
Active goals are now demodulated after selecting a positive clause.
Implemented OrderedSet for passive clauses.
Selection is now based on weight (fairness condition to be added).

15 years ago- applyTransformation: bugfix in the rendering of records
Ferruccio Guidi [Thu, 11 Jun 2009 22:02:51 +0000 (22:02 +0000)]
- applyTransformation: bugfix in the rendering of records

now algebra/monoids.ma is fully reconstructed :)

15 years agocontent2pres for the new cic fixed
Enrico Tassi [Thu, 11 Jun 2009 13:57:41 +0000 (13:57 +0000)]
content2pres for the new cic fixed

15 years ago- some depend files fixed
Ferruccio Guidi [Thu, 11 Jun 2009 12:59:35 +0000 (12:59 +0000)]
- some depend files fixed
- matitacLib: we peform a garbage collection after compiling every file instead of just .mma (let's see the times)
- transcript: support for "cr" inline param completed
- procedural: now record are supported

the records of logic/cprop_coonectives.ma are now reconstructed :)

logic higher_order_defs list nat Z Q are now fully reconstructed :))

15 years ago- library/list/list.ma: unused code commented
Ferruccio Guidi [Wed, 10 Jun 2009 20:19:42 +0000 (20:19 +0000)]
- library/list/list.ma: unused code commented
- proceduralClassify type argument are no longer critical: let's see how it goes
- acic2Procedural: the inline parameter Debug now works
- procedural2: we remove the conversions before first order relexivities (exp. to avoid conversion to []=[] in list/list.ma [does not work because []=[] in an open term since the equality type is unspecified]). so we we strengthen reflexivity (see below)
- setoids: now reflexivity is retried after whd if it fails in the first place.
- grafiteAst: detection of convertible rewrites is now optional and activated with the inline parameter "cr". nat/factorial2 is very slow without rewrites
transcript: we now avoid the generation of dupplicated inlines (mistakely generated by the grafite parser [this can not be avoided without a better syntax for .ma scripts])

now list/list.ma is fully reconstructed :)

nat/factorial2.ma takes long to be produced 22m31. Some conversion is slowing the process. nat/bertrand.ma also: we are waiting for it now :(

15 years ago1) added simplification of actives w.r.t. selected
Enrico Tassi [Wed, 10 Jun 2009 16:43:48 +0000 (16:43 +0000)]
1) added simplification of actives w.r.t. selected
2) added simple main loop (look at the comment for a possible optimization)

15 years agoright inference step completed
Enrico Tassi [Wed, 10 Jun 2009 13:38:08 +0000 (13:38 +0000)]
right inference step completed

15 years agonew function filter_map_acc
Enrico Tassi [Wed, 10 Jun 2009 11:39:26 +0000 (11:39 +0000)]
new function filter_map_acc

15 years agoExtended the equality case to non ground terms
denes [Wed, 10 Jun 2009 08:46:55 +0000 (08:46 +0000)]
Extended the equality case to non ground terms

15 years ago- Procedural: more support for the Debug inline option (does not work yet)
Ferruccio Guidi [Tue, 9 Jun 2009 17:22:52 +0000 (17:22 +0000)]
- Procedural: more support for the Debug inline option (does not work yet)
- transcript: now we can process a given subset so the source files
- termContentPres: bugfix in the syntax of letrec, a space was missing :(

now nat/generic_iter_p.ma is fully reconstructed :) (thx Claudio)

15 years agoDebugging code removed.
Claudio Sacerdoti Coen [Tue, 9 Jun 2009 16:59:24 +0000 (16:59 +0000)]
Debugging code removed.

15 years agoTemporary (and partially broken) patch for Ferruccio: I duplicate
Claudio Sacerdoti Coen [Tue, 9 Jun 2009 16:37:54 +0000 (16:37 +0000)]
Temporary (and partially broken) patch for Ferruccio: I duplicate
\Pi abstractions in let ... rec definitions in order to make the system
infer the same names. However, it could be infer a -> in place of a \forall.

15 years agoalmost complete superposition right step
Enrico Tassi [Tue, 9 Jun 2009 16:22:41 +0000 (16:22 +0000)]
almost complete superposition right step

15 years agosnapshot
Enrico Tassi [Tue, 9 Jun 2009 15:09:42 +0000 (15:09 +0000)]
snapshot

15 years agosee the previous commit
Enrico Tassi [Tue, 9 Jun 2009 15:01:30 +0000 (15:01 +0000)]
see the previous commit

15 years agotermAcicContent is logic independent (despite its name) thus it
Enrico Tassi [Tue, 9 Jun 2009 14:56:01 +0000 (14:56 +0000)]
termAcicContent is logic independent (despite its name) thus it
needs also term_of_nref

15 years agoOptimized weigths comparison, removed normalization
denes [Tue, 9 Jun 2009 13:31:02 +0000 (13:31 +0000)]
Optimized weigths comparison, removed normalization

15 years agosnaphost: supright almost done
Enrico Tassi [Tue, 9 Jun 2009 13:17:31 +0000 (13:17 +0000)]
snaphost: supright almost done

15 years ago...
Enrico Tassi [Tue, 9 Jun 2009 13:17:14 +0000 (13:17 +0000)]
...

15 years ago...
Enrico Tassi [Tue, 9 Jun 2009 13:16:05 +0000 (13:16 +0000)]
...

15 years agoImplemented substitution application and concatenation
denes [Tue, 9 Jun 2009 13:15:58 +0000 (13:15 +0000)]
Implemented substitution application and concatenation

15 years ago...
Enrico Tassi [Tue, 9 Jun 2009 13:15:18 +0000 (13:15 +0000)]
...

15 years agofixed metas
Enrico Tassi [Tue, 9 Jun 2009 09:54:56 +0000 (09:54 +0000)]
fixed metas

15 years agofixed building
Enrico Tassi [Tue, 9 Jun 2009 09:54:36 +0000 (09:54 +0000)]
fixed building

15 years ago...
Enrico Tassi [Mon, 8 Jun 2009 18:56:48 +0000 (18:56 +0000)]
...

15 years agoa skeleton of supright
Enrico Tassi [Mon, 8 Jun 2009 17:27:16 +0000 (17:27 +0000)]
a skeleton of supright

15 years agosome more functors and a nice higher-order all_positions iterator
Enrico Tassi [Mon, 8 Jun 2009 16:34:39 +0000 (16:34 +0000)]
some more functors and a nice higher-order all_positions iterator

15 years agoadded META for ng_paramodulation
Enrico Tassi [Mon, 8 Jun 2009 13:04:29 +0000 (13:04 +0000)]
added META for ng_paramodulation

15 years agoPrevious commit reverted, as explained in that log.
Claudio Sacerdoti Coen [Sat, 6 Jun 2009 16:45:12 +0000 (16:45 +0000)]
Previous commit reverted, as explained in that log.

15 years agoThis commit restores the ids_to_father_ids table.
Claudio Sacerdoti Coen [Sat, 6 Jun 2009 16:43:35 +0000 (16:43 +0000)]
This commit restores the ids_to_father_ids table.
However, after the implementation, I sort of realized that maybe this table
is useless, after all.
Thus I am gonna do my commit and immediately revert it (just to keep the
code in SVN in case of need).

15 years agosome renaming to make ocamlopt happy
Enrico Tassi [Sat, 6 Jun 2009 08:59:51 +0000 (08:59 +0000)]
some renaming to make ocamlopt happy

15 years agobugfix in Include syntax: it was changed and committed by mistake :(
Ferruccio Guidi [Fri, 5 Jun 2009 22:23:42 +0000 (22:23 +0000)]
bugfix in Include syntax: it was changed and committed by mistake :(

15 years ago- Procedural convertible rewrites in the conclusion are now detected and replaced...
Ferruccio Guidi [Fri, 5 Jun 2009 22:18:01 +0000 (22:18 +0000)]
- Procedural convertible rewrites in the conclusion are now detected and replaced by change
- grafiteAst: semantics of the Include flag changed: now true means normal include, New Inline flags Coercions, Comments (activated) Debug (not yet)
- library: eq_plus_Zplus moved from Z/times to Z/plus

now Z/plus.ma Z/times.ma are fully reconstructed :)

15 years agoFirst tests for paramodulation (pretty printer, unification)
denes [Fri, 5 Jun 2009 15:33:35 +0000 (15:33 +0000)]
First tests for paramodulation (pretty printer, unification)

15 years ago- replaced part1a/defn with the version based on induction/inversion and deleted
Wilmer Ricciotti [Fri, 5 Jun 2009 13:27:14 +0000 (13:27 +0000)]
- replaced part1a/defn with the version based on induction/inversion and deleted
older version
- more minor improvements

15 years agoFix : wrong exception was catch in apply_subst
denes [Fri, 5 Jun 2009 12:25:06 +0000 (12:25 +0000)]
Fix : wrong exception was catch in apply_subst

15 years ago1) the home button of CicBrowser now works also for NG
Claudio Sacerdoti Coen [Fri, 5 Jun 2009 09:52:20 +0000 (09:52 +0000)]
1) the home button of CicBrowser now works also for NG
2) implemented simple (i.e. no natural language) rendering of NG constants.
   Inductive types and (co)recursive definitions are still missing.

15 years agoThe kernel _must_ check the correctness of the height since the reduction
Claudio Sacerdoti Coen [Fri, 5 Jun 2009 08:56:17 +0000 (08:56 +0000)]
The kernel _must_ check the correctness of the height since the reduction
machine never tries to reduce terms whose height is 0. Thus, if the
declared height is 0, the height is no longer an optimization!

15 years agosyntax error fixed :(
Ferruccio Guidi [Thu, 4 Jun 2009 18:41:36 +0000 (18:41 +0000)]
syntax error fixed :(

15 years ago- doubleTypeInference: we check for unreferenced letins in the inferred type also...
Ferruccio Guidi [Thu, 4 Jun 2009 18:35:24 +0000 (18:35 +0000)]
- doubleTypeInference: we check for unreferenced letins in the inferred type also after beta-reduction because beta-reduction can cause unreferenced letins
- procedural: bugfix in the use of inner types, the expected type was sometimes used in place of the inferred type; context cleaning is now disabled because the clear tactics are not generated; debugging mode is now activated

nat/ord.ma is now fully reconstructed :)

15 years agoFirst pretty printing functions
denes [Thu, 4 Jun 2009 13:57:56 +0000 (13:57 +0000)]
First pretty printing functions

15 years agominor changes here and there. We extend fo-unification with
Enrico Tassi [Thu, 4 Jun 2009 10:19:04 +0000 (10:19 +0000)]
minor changes here and there. We extend fo-unification with
(X ...) =?= (f ...) --> X := f

15 years agocomments
Enrico Tassi [Thu, 4 Jun 2009 10:18:12 +0000 (10:18 +0000)]
comments

15 years agobetter type for comparison and implementation of KBO orderings
Enrico Tassi [Thu, 4 Jun 2009 09:52:15 +0000 (09:52 +0000)]
better type for comparison and implementation of KBO orderings

15 years agomore functors
Enrico Tassi [Thu, 4 Jun 2009 08:09:31 +0000 (08:09 +0000)]
more functors

15 years ago- boxPp: added missing spaces
Ferruccio Guidi [Wed, 3 Jun 2009 20:20:11 +0000 (20:20 +0000)]
- boxPp: added missing spaces
- core_notation: bug fix in the input notation for congruent: we added term 90 after \sub
- library/nat/permutation.ma: added input notation for transpose and fixed term precedence in its output notation
- library/Makefile: compilation of single files re-enabled.
The syntax for compiling file.ma is is "make file.mo" and "make file.mo.opt"

now nat/congruence.ma and nat/permutation.ma are fully reconstructed :)

15 years agoUpdate, using induction/inversion.
Wilmer Ricciotti [Wed, 3 Jun 2009 16:47:25 +0000 (16:47 +0000)]
Update, using induction/inversion.

15 years agofunctorial abstraction over term blobs
Enrico Tassi [Wed, 3 Jun 2009 15:37:06 +0000 (15:37 +0000)]
functorial abstraction over term blobs

15 years agonot_to_not
Andrea Asperti [Wed, 3 Jun 2009 14:42:12 +0000 (14:42 +0000)]
not_to_not

15 years agoNew test for NG notation.
Claudio Sacerdoti Coen [Wed, 3 Jun 2009 08:57:56 +0000 (08:57 +0000)]
New test for NG notation.

15 years agoHuge commit with several changes:
Claudio Sacerdoti Coen [Wed, 3 Jun 2009 08:56:58 +0000 (08:56 +0000)]
Huge commit with several changes:

1) CicNotationPres.render: type changed to make it more general (no
   dependency on the Hashtbl) and URI/REFERENCE agnostic.
   A compatibility function CicNotationPres.lookup_uri is provided to
   easily map the (old) Hashtbl to the (new) lookup function.
2) user interface partially changed to render NG objects in the CicBrowser
   and to follow NG hyperlinks
3) New CicNotationPt entries NRef (similar to Uri) and NRefPattern
   (similar to UriPattern) to avoid hijacking the old Uris (actually,
   uris + xpointers) to also hold new references.
   This allows to properly implement notation (for NG) and to properly
   handle hyperlinks.
4) all remaining Warnings for unused variables fixed (in some way or
   another, hopefully the correct one)
5) GrafiteEngine, NQed: the height of an object is now recomputed just
   before putting it in the environment. This fixes all the bugs related
   to reduction.
6) GrafiteParser/LexiconEngine: both old URIs and new references are now
   allowed in NG terms and in notations
7) ng_cic_content: rendering functions now return an "id |-> reference" table
   to correctly implement MathML hrefs
8) NReference: new compare function
9) NCicUntrusted: new height_of_obj_kind function (to be used in GrafiteEngine)
10) OCic2NCic: new reference_of_oxuri function to map old uris + xpointers
   into new references
11) bug fixed: after the commit by Enrico that starts using the extensible
   PTS, the old-to-new objects translations used to map Type into "Type" which
   was not declared. Type is now mapped into Type[0] and Type (as a "notation")
   is now a synonim of Type[0] (only during parsing for now)
12) bug fixed: after the commit by Enrico that cleans up terms for
    alpha-conversion and dummy products, the test in NCicTypeChecker that
    verifies the consistency of left parameters in constructor --- that used
    to do that NOT up to alpha-conversion --- used to fail when dummy products
    were found. The test is now relaxed to include alpha-conversion.
13) bug fixed: NCicTypeChecker did not verify that a .dec reference pointed to
    an axiom and that a .def reference did not point to an axiom. Fixed.

15 years agoFirst implementation of unification on foterms
denes [Mon, 1 Jun 2009 16:36:42 +0000 (16:36 +0000)]
First implementation of unification on foterms

15 years agoFirst functions on substitutions for unification
denes [Mon, 1 Jun 2009 15:32:18 +0000 (15:32 +0000)]
First functions on substitutions for unification

15 years agoadded a snapshot of comparison
Enrico Tassi [Mon, 1 Jun 2009 13:49:20 +0000 (13:49 +0000)]
added a snapshot of comparison

15 years agoThis works for me
Andrea Asperti [Mon, 1 Jun 2009 12:23:46 +0000 (12:23 +0000)]
This works for me

15 years agowe rewrite the paramodulation code!
Enrico Tassi [Mon, 1 Jun 2009 11:57:04 +0000 (11:57 +0000)]
we rewrite the paramodulation code!

15 years agoPOPLmark part 1a using the de Bruijn encoding.
Wilmer Ricciotti [Fri, 29 May 2009 15:08:59 +0000 (15:08 +0000)]
POPLmark part 1a using the de Bruijn encoding.

15 years ago- cicNotationParser: added extra space to TeX control sequences accordind to previous...
Ferruccio Guidi [Fri, 29 May 2009 14:26:50 +0000 (14:26 +0000)]
- cicNotationParser: added extra space to TeX control sequences accordind to previous commit of cicNotationLexer
- core_notation: bugfix in the notation for exp
- library/nat/congruence.ma: notation for "congruent" moved to core_notation

now nat/exp.ma is fully reconstructed :)

15 years agoProcedural: higher-order unification needs a lot of hints !!
Ferruccio Guidi [Thu, 28 May 2009 18:15:13 +0000 (18:15 +0000)]
Procedural: higher-order unification needs a lot of hints !!

files fully reconstructed today:
nat/lt_arith.ma nat/div_and_mod.ma Z/plus.ma Z/orders.ma

15 years ago- cicInspect: relevant nodes count updated: letin nodes are not relevant
Ferruccio Guidi [Thu, 28 May 2009 17:17:29 +0000 (17:17 +0000)]
- cicInspect: relevant nodes count updated: letin nodes are not relevant
- Procedural: reflexivity is now supported
- grafiteAst: boolean flag for include to tag inclusion of a source file. This command is relevant for .ma generation only. [ the source file of a .mma is not included in the generated .ma ]
- cicNotationLexer: unexpanded TeX macro symbols are now encoded with an extra space at the end. This is consistent with the concept of TeX sequence and fixes a bug in the renering of these symbols. The space is needed for reparsing!

15 years agoProcedural: bugfix in the generation of intros for letin: the bodies and types of...
Ferruccio Guidi [Wed, 27 May 2009 18:44:41 +0000 (18:44 +0000)]
Procedural: bugfix in the generation of intros for letin: the bodies and types of the actual letin and of the inferred letin must be equal upto alpha

now nat/minus.ma and nat/minimization.ma are fully reconstructed :)

15 years ago- Procedural: we specify more unifiers for apply to help higher-order unification
Ferruccio Guidi [Wed, 27 May 2009 17:16:31 +0000 (17:16 +0000)]
- Procedural: we specify more unifiers for apply to help higher-order unification
- cicNotationPp: bugfix in the notation for Meta and ImplicitPattern
- transcript: grafite lexer/parser updated

15 years agoBasic support for interpretations for NG:
Claudio Sacerdoti Coen [Wed, 27 May 2009 08:49:30 +0000 (08:49 +0000)]
Basic support for interpretations for NG:
 1) only interpretations for old objects are used
    (i.e. no way yet to declare a new interpretation on a new object)
 2) only interpretations for constants (no inductive definitions/constructors)
    since we have no faithful embedding of new references into old URIs
 3) no support for backtracking (I think)

15 years agoAvoiding to filter the application of congruence equations
Andrea Asperti [Wed, 27 May 2009 06:38:45 +0000 (06:38 +0000)]
Avoiding to filter the application of congruence equations
due to a couple of cases in "didactics" where auto is used
instead of reflexivity.

15 years ago...
Claudio Sacerdoti Coen [Tue, 26 May 2009 11:52:47 +0000 (11:52 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Tue, 26 May 2009 11:45:48 +0000 (11:45 +0000)]
...

15 years agoremoved a call to autobatch.
Andrea Asperti [Tue, 26 May 2009 10:47:42 +0000 (10:47 +0000)]
removed a call to autobatch.

15 years agonasty change in the lexer/parser:
Enrico Tassi [Mon, 25 May 2009 15:39:26 +0000 (15:39 +0000)]
nasty change in the lexer/parser:
- identifiers can begin with _
- interpretations use ? for implicits instead of _

possible problems:
- _foo is not anymore: SYMBOL(_) IDENT(foo)
  put a space to obtain the old token stream

15 years agobugfix in the output notation for eq
Ferruccio Guidi [Fri, 22 May 2009 12:17:28 +0000 (12:17 +0000)]
bugfix in the output notation for eq

15 years agoPruning candidates in the applicative case for equalities.
Andrea Asperti [Fri, 22 May 2009 11:15:56 +0000 (11:15 +0000)]
Pruning candidates in the applicative case for equalities.

15 years agoProcedural: we use the expected type rather than the inferred type when we perform...
Ferruccio Guidi [Thu, 21 May 2009 19:04:29 +0000 (19:04 +0000)]
Procedural: we use the expected type rather than the inferred type when we perform a cut to keep the goal in sync with the expected type.
we try to beta-reduce the elimination pattern when it does not match the goal/expected type

now nat/compare.ma and Z/z.ma are fully reconstructed :)

15 years ago- cicUtil: is_sober now detects non-positive rels.
Ferruccio Guidi [Thu, 21 May 2009 12:45:14 +0000 (12:45 +0000)]
- cicUtil: is_sober now detects non-positive rels.
- PropceduralOptimizer: bug fix in critical step detection

now decidable_kit/streicher.ma is fully reconstructed :)

15 years agoautobatch -> autobatch by
Andrea Asperti [Thu, 21 May 2009 11:42:28 +0000 (11:42 +0000)]
autobatch -> autobatch by

15 years agowe catch the refiner errors in the critical step and fall back to the non-criticall...
Ferruccio Guidi [Wed, 20 May 2009 20:44:49 +0000 (20:44 +0000)]
we catch the refiner errors in the critical step and fall back to the non-criticall version (this is just for debugging)
bug-fix in elimination recognition euristics

now nat/orders.ma and nat/times.ma are fully reconstructed :)

15 years agoRemoved a silly type check
Andrea Asperti [Wed, 20 May 2009 15:35:12 +0000 (15:35 +0000)]
Removed a silly type check

15 years ago...
Enrico Tassi [Tue, 19 May 2009 14:38:16 +0000 (14:38 +0000)]
...

15 years agoNotEq is now considered as a negative Eq atom
Andrea Asperti [Tue, 19 May 2009 14:34:01 +0000 (14:34 +0000)]
NotEq is now considered as a negative Eq atom

15 years agoregenerated
Enrico Tassi [Tue, 19 May 2009 10:07:50 +0000 (10:07 +0000)]
regenerated

15 years agofixed generation of horn clauses, negated atoms are hypotheses
Enrico Tassi [Tue, 19 May 2009 10:07:42 +0000 (10:07 +0000)]
fixed generation of horn clauses, negated atoms are hypotheses

15 years agosome horn+equality problems
Enrico Tassi [Tue, 19 May 2009 09:42:47 +0000 (09:42 +0000)]
some horn+equality problems

15 years agoremoved byte queries
Claudio Sacerdoti Coen [Mon, 18 May 2009 22:08:17 +0000 (22:08 +0000)]
removed byte queries

15 years agoremoved useless function
Enrico Tassi [Mon, 18 May 2009 15:28:48 +0000 (15:28 +0000)]
removed useless function

15 years agoin the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as
Enrico Tassi [Mon, 18 May 2009 15:25:52 +0000 (15:25 +0000)]
in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as
Type[0]. The same holds for CProp.

tests/ng_pts.ma defines some sorts, you may want to include it

15 years agonothing special
Enrico Tassi [Mon, 18 May 2009 15:04:07 +0000 (15:04 +0000)]
nothing special

15 years ago1) GrafiteAst.NEval => GrafiteAst.NReduce
Claudio Sacerdoti Coen [Mon, 18 May 2009 11:59:53 +0000 (11:59 +0000)]
1) GrafiteAst.NEval => GrafiteAst.NReduce
2) new tactic "nnormalize" implemented
3) "ngeneralize" now uses "wanted" when no term is selected
   (so that it is possible to use ngeneralize to move an
   hypothesis down)
4) new syntax for non punctuational tinycals was missing

15 years ago1) new tactic normalize (low-level function implemented in
Claudio Sacerdoti Coen [Mon, 18 May 2009 11:57:50 +0000 (11:57 +0000)]
1) new tactic normalize (low-level function implemented in
   nCicTacReduction)
2) the select tactic used to generate fresh metavariables by unifying the
   "wanted" part of the pattern in a root where "wanted" did not occur.
   Those metavariables are now removed in that case