]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

15 years ago1) order of processing of case branches reverted (to generate metas in
Claudio Sacerdoti Coen [Mon, 18 May 2009 11:54:20 +0000 (11:54 +0000)]
1) order of processing of case branches reverted (to generate metas in
   left-to-right order)
2) metas generated by eat_prods are now re-ordered so that they occur
   in left-to-right order

15 years agomaxmeta implemented
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:13:21 +0000 (19:13 +0000)]
maxmeta implemented

15 years agomaxmeta function to return the heighest meta used so far
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:13:03 +0000 (19:13 +0000)]
maxmeta function to return the heighest meta used so far

15 years agoalpha_eq exported
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:12:33 +0000 (19:12 +0000)]
alpha_eq exported

15 years agoalpha_eq defined and exported
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:12:15 +0000 (19:12 +0000)]
alpha_eq defined and exported

15 years agoefficiency improvement (buffers are now used everywhere)
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:11:41 +0000 (19:11 +0000)]
efficiency improvement (buffers are now used everywhere)

15 years ago...
Claudio Sacerdoti Coen [Sun, 17 May 2009 19:11:00 +0000 (19:11 +0000)]
...

15 years agobyte tests disabled
Enrico Tassi [Sun, 17 May 2009 18:43:33 +0000 (18:43 +0000)]
byte tests disabled

15 years agoadded patch to not unify any term containing the in_scope tag with
Enrico Tassi [Fri, 15 May 2009 21:14:15 +0000 (21:14 +0000)]
added patch to not unify any term containing the in_scope tag with
an entry in the local context

15 years agoPatch to add a debugging string to HExtlib.split_nth reverted
Claudio Sacerdoti Coen [Fri, 15 May 2009 19:37:08 +0000 (19:37 +0000)]
Patch to add a debugging string to HExtlib.split_nth reverted
(we cannot add a string to every function that raises an exception).

To know where the problem is, it is sufficient to look at the backtrace.
However:
 1) it works for matitac -debug
 2) ocaml is so dumb that it says "compile with -g" when it cannot find
    the executable in the current working directory. Since Matita chdir
    to the directory where the .ma file is, you need to put a copy of
    matitac (or make a symbolic link) where the .ma file is.

15 years agoCosmetic.
Claudio Sacerdoti Coen [Fri, 15 May 2009 19:34:31 +0000 (19:34 +0000)]
Cosmetic.

15 years ago- hExtlib: added debugging information for split_nth
Ferruccio Guidi [Thu, 14 May 2009 14:32:39 +0000 (14:32 +0000)]
- hExtlib: added debugging information for split_nth

nat/plus.ma reconstructed :)

15 years ago- libraryObjects: new default "natural numbers" with the uri of nat.
Ferruccio Guidi [Thu, 14 May 2009 13:43:55 +0000 (13:43 +0000)]
- libraryObjects: new default "natural numbers" with the uri of nat.
alias num "natural number" uses this one instead of the hardcoded uri (removed)
also destroy_nat (moved to termAcicContent) looks at this default

15 years agointerpretations placed right after the corresponding definitions (in this way the...
Ferruccio Guidi [Wed, 13 May 2009 19:30:53 +0000 (19:30 +0000)]
interpretations placed right after the corresponding definitions (in this way the script is reconstructed correctly)

logic/equality and datatypes/bool reconstructed :)

15 years ago- matitaEngine: some commands like "coercion" must not be executed when mma's are...
Ferruccio Guidi [Wed, 13 May 2009 18:44:42 +0000 (18:44 +0000)]
- matitaEngine: some commands like "coercion" must not be executed when mma's are dumped. This hack will be removed when mma's will be executed while dumped
- primitiveTactics: bugxix in the generation of the predicate for elim: we leave to the refiner the task of instantiating the types of the pattern variables.
Note: the head beta-reductions after the elimination must be performed following the instantiated predicate because (\lambda x:?.t v) does not beta-reduce (bug or feature?)

15 years agoThe singature of the "by" universe is added to the goal signature
Andrea Asperti [Wed, 13 May 2009 15:19:18 +0000 (15:19 +0000)]
The singature of the "by" universe is added to the goal signature
(so univ is never filtered)

15 years agoVia un'altra linea...
Andrea Asperti [Wed, 13 May 2009 09:55:04 +0000 (09:55 +0000)]
Via un'altra linea...

15 years agoSempre piu' breve
Andrea Asperti [Wed, 13 May 2009 09:37:51 +0000 (09:37 +0000)]
Sempre piu' breve

15 years agoSignature is computed on the initial goal, once and for all.
Andrea Asperti [Wed, 13 May 2009 09:27:34 +0000 (09:27 +0000)]
Signature is computed on the initial goal, once and for all.
Ripristined the filtering on candidates also for non-smart applications
(was too slow on some examples, e.g. in Fsub *

15 years agoDo we really want to generate eliminators for nested data types? :-)
Claudio Sacerdoti Coen [Tue, 12 May 2009 22:16:00 +0000 (22:16 +0000)]
Do we really want to generate eliminators for nested data types? :-)

15 years agoAll weakly positive types but imbricated ones are now accepted
Claudio Sacerdoti Coen [Tue, 12 May 2009 21:37:40 +0000 (21:37 +0000)]
All weakly positive types but imbricated ones are now accepted
(e.g. ordinals).

15 years ago- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...
Ferruccio Guidi [Tue, 12 May 2009 19:04:32 +0000 (19:04 +0000)]
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal starts with an abbreviation. Clearbody before change in reactivated (to change the inferred type of the abbreviations of sort Prop)
- RELATIONAL: notation fixup
- character: autobatch fixup
- ng_tactics: dependences were not committed correctly

15 years agoWe only filter the smart candidates w.r.t the signature
Andrea Asperti [Tue, 12 May 2009 13:56:17 +0000 (13:56 +0000)]
We only filter the smart candidates w.r.t the signature

15 years agoSome experiments in generation of elimination principles.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:47:29 +0000 (21:47 +0000)]
Some experiments in generation of elimination principles.

15 years agoppsubst commented out in ppobj
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:46:42 +0000 (21:46 +0000)]
ppsubst commented out in ppobj

15 years agoBug fixed: the relevance list can be shorted then leftno args.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:45:30 +0000 (21:45 +0000)]
Bug fixed: the relevance list can be shorted then leftno args.

15 years agoMissing spaces inserted here and there.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:45:00 +0000 (21:45 +0000)]
Missing spaces inserted here and there.

15 years ago- non_punctuational_tacticals ported to NG
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:44:34 +0000 (21:44 +0000)]
- non_punctuational_tacticals ported to NG
- experimental generation of elimination principles passing through ASTs

15 years agoBuffers are now used everywhere for speed-up.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:42:45 +0000 (21:42 +0000)]
Buffers are now used everywhere for speed-up.
However, the ppsubst is deadly slow even for not-that-large substitutions.

15 years agoNew function list_iter_sep.
Claudio Sacerdoti Coen [Mon, 11 May 2009 21:42:08 +0000 (21:42 +0000)]
New function list_iter_sep.

15 years agoA few lemmas about inclusion.
Andrea Asperti [Mon, 11 May 2009 16:20:24 +0000 (16:20 +0000)]
A few lemmas about inclusion.

15 years agoMore automation
Andrea Asperti [Mon, 11 May 2009 16:19:42 +0000 (16:19 +0000)]
More automation

15 years ago- critical bug fixed in NCicSubstitution.lift:
Claudio Sacerdoti Coen [Sun, 10 May 2009 10:51:06 +0000 (10:51 +0000)]
- critical bug fixed in NCicSubstitution.lift:
  (0,Irl 0) was lifted to (1,Irl 0)
  but later on NCicTypechecker.check_metasenv_consistency assumes the
  invariant that the currenct context has length (m+n) if the metavariable
  is (m,Irl n). But this invariant is false in the case (m, Irl 0) when m > 0.
- in NCicRefiner there was one line to normalize (m,Irl 0) and (m,Ctx []) to
  (0,...). Is it still required after the first patch to the kernel? I suspect
  no, thus I put an assert false to check.

15 years agoStupid typing error fixed.
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:27:02 +0000 (22:27 +0000)]
Stupid typing error fixed.

15 years ago...
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:26:18 +0000 (22:26 +0000)]
...

15 years ago...
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:25:59 +0000 (22:25 +0000)]
...

15 years agoBug fixed: left parameters of constructors were unified before refining them.
Claudio Sacerdoti Coen [Fri, 8 May 2009 22:07:55 +0000 (22:07 +0000)]
Bug fixed: left parameters of constructors were unified before refining them.
Fixed, but the new code typechecks the constructors twice (in order to
re-compute) the sort without the inductive types. Is a more efficient
implementation worth the effort?

15 years agoBug fixed: refinement of mutual recursive definitions used to invert the
Claudio Sacerdoti Coen [Fri, 8 May 2009 21:20:22 +0000 (21:20 +0000)]
Bug fixed: refinement of mutual recursive definitions used to invert the
definitions.

15 years agoImproved tests (for left parameters and mutual recursive definitions).
Claudio Sacerdoti Coen [Fri, 8 May 2009 21:06:29 +0000 (21:06 +0000)]
Improved tests (for left parameters and mutual recursive definitions).

15 years agoBug fixed in refinement of inductive types: left parameters were forgot
Claudio Sacerdoti Coen [Fri, 8 May 2009 18:05:00 +0000 (18:05 +0000)]
Bug fixed in refinement of inductive types: left parameters were forgot
during reconstruction of refined object.

15 years ago1) better implementation of NObj that now calls recursively NQed
Claudio Sacerdoti Coen [Fri, 8 May 2009 16:47:23 +0000 (16:47 +0000)]
1) better implementation of NObj that now calls recursively NQed
   to avoid code duplication
2) NQed now calls the kernel to check the object, since add_obj is too
   low level for that (this makes a huge difference with the previous
   architecture, but will probably break when dealing with undo)

15 years agoThe relevance list can be shorter than leftno (when the default is used).
Claudio Sacerdoti Coen [Fri, 8 May 2009 16:29:45 +0000 (16:29 +0000)]
The relevance list can be shorter than leftno (when the default is used).

15 years agoBug fixed in interpretation of records (the type was unbound in the fields).
Claudio Sacerdoti Coen [Fri, 8 May 2009 15:00:03 +0000 (15:00 +0000)]
Bug fixed in interpretation of records (the type was unbound in the fields).

15 years agoConstructors are closed with thier types when computing the signatur
Andrea Asperti [Fri, 8 May 2009 14:50:27 +0000 (14:50 +0000)]
Constructors are closed with thier types when computing the signatur

15 years agoversione automatizzata
Andrea Asperti [Fri, 8 May 2009 14:40:41 +0000 (14:40 +0000)]
versione automatizzata

15 years agosymmetry of inequality sym_neq
Andrea Asperti [Fri, 8 May 2009 14:39:54 +0000 (14:39 +0000)]
symmetry of inequality sym_neq

15 years agodocumentation for the inline command
Ferruccio Guidi [Thu, 7 May 2009 14:30:26 +0000 (14:30 +0000)]
documentation for the inline command

15 years ago- dependenciesParser: updated to new inline syntax
Ferruccio Guidi [Wed, 6 May 2009 19:20:32 +0000 (19:20 +0000)]
- dependenciesParser: updated to new inline syntax

15 years agoLAMBDA-TYPES: mma's recommitted because inline syntax changed
Ferruccio Guidi [Wed, 6 May 2009 19:01:31 +0000 (19:01 +0000)]
LAMBDA-TYPES: mma's recommitted because inline syntax changed

15 years ago- cicUtil: is_sober now detects folded applications
Ferruccio Guidi [Wed, 6 May 2009 18:26:56 +0000 (18:26 +0000)]
- cicUtil: is_sober now detects folded applications
- Procedural: bugfix in pattern generation for elim/rewrite, better debug output, applications are flattened before alpha-conversion to hide a bug of the double type inference :( (it generates folded applications)
- applyTransformation: coercions are shown when rendering a tactic because Procedural is not aware of coercions :(