]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
better tex/utf8 win
[helm.git] / helm / software / components /
2008-07-22 Ferruccio Guidimatitadep: we now handle the inline of an uri, we remov...
2008-07-22 Ferruccio Guiditranscript: now we can generate procedural output
2008-07-21 Claudio Sacerdoti... Error message improved.
2008-07-21 Claudio Sacerdoti... Rendering of \infrule improved.
2008-07-21 Ferruccio Guidiwe implemented the support for generating ma files...
2008-07-21 Enrico Tassiavoid empty hvbox
2008-07-18 Enrico Tassibetter metavariable context
2008-07-18 Enrico Tassimetavariable context has a separator now
2008-07-18 Enrico Tassiexception inside regex callback not re-raised if equal...
2008-07-17 Claudio Sacerdoti... Bugs fixed:
2008-07-16 Ferruccio GuidiProcedural: some comments added in the generated script
2008-07-16 Enrico Tassinotations for lists adds some breaking points
2008-07-15 Ferruccio Guidicic2acic: new function acic_term_of_cic_term
2008-07-15 Enrico TassiCProp_i <= Type_i , Type_i <= CProp_i
2008-07-14 Ferruccio Guidilambda-delta: we added the support for position indexes...
2008-07-14 Ferruccio GuidiProcedural: we added the support for rendering definiti...
2008-07-13 Ferruccio GuidiProcedural: we added the support for theorem flavours...
2008-07-13 Ferruccio GuidicicUtil : we added a context to is_sober...
2008-07-12 Ferruccio GuidiProcedural: bug fix in the procedural rendering of...
2008-07-12 Ferruccio Guidilibrarian: retrieval of buildable files speeded up...
2008-07-12 Claudio Sacerdoti... New feature/bug fixed (hopefully): it is now possible...
2008-07-11 Claudio Sacerdoti... Exists is no longer an ad-hoc notation hard-coded in...
2008-07-11 Claudio Sacerdoti... Added new ternary layout \infrule premises conclusion...
2008-07-10 Enrico Tassifixed regression in casting an argument to funclass...
2008-07-09 Ferruccio Guidisome bug fixes
2008-07-09 Enrico TassiCProp hierarchy fixed:
2008-07-09 Enrico Tassitab -> ' '
2008-07-07 Enrico Tassisimplified coercDb implementation with additional info...
2008-07-04 Ferruccio Guidi- we replaced a normalize with a whd in the classificat...
2008-07-04 Ferruccio Guidi- Procedural: bug fix in rendering the application...
2008-07-02 Ferruccio Guidi- new tactic applyP for use in the *P*rocedural script...
2008-07-02 Wilmer RicciottiFixed a bug which prevented mutually recursive definiti...
2008-07-02 Enrico Tassicalculation of the sort user to choose the rewriting...
2008-06-25 Enrico Tassibetter, reparsable, notation
2008-06-24 Enrico Tassinotation factored, coercion commant taking terms and...
2008-06-24 Enrico Tassimissing file added
2008-06-23 Enrico Tassiadd \\ in front of tex macros
2008-06-23 Enrico Tassinotation support fixed to parentesize in a more sane...
2008-06-22 Ferruccio Guidi- grafiteParser.ml: the callback invocation was displaced
2008-06-20 Claudio Sacerdoti... - partial implementation of pattern for case documented
2008-06-19 Enrico Tassinotation fixed to be NON associative by default
2008-06-19 Claudio Sacerdoti... 1. bug fixed in generalize_pattern: a lazy const_tac...
2008-06-19 Ferruccio Guidi- Procedural: we now check that an eliminator opens...
2008-06-19 Enrico Tassinotation on steroids: 'term 40 x' is a valid variable...
2008-06-18 Enrico Tassiinitial support for notation that specifies the precede...
2008-06-17 Enrico Tassireordering of lexicon status partially avoided to make...
2008-06-13 Wilmer Ricciottifinal relevance check
2008-06-13 Enrico Tassireplace assert false with AssertFailure
2008-06-13 Enrico Tassiprint the name not found in the env
2008-06-11 Enrico Tassimeta not considered before in outtype
2008-06-10 Wilmer Ricciottirelevance check for Match
2008-06-10 Wilmer RicciottiAdded check of relevance lists for inductive types...
2008-06-09 Claudio Sacerdoti... It is now possible to use identifiers in place of URI...
2008-06-09 Wilmer RicciottiReverting to the previous version some files which...
2008-06-09 Wilmer Ricciottimore proof irrelevance
2008-06-08 Claudio Sacerdoti... Bug fixed: wrong default pattern for generalize.
2008-06-08 Claudio Sacerdoti... Hypotheses patterns for elim implemented. No more need...
2008-06-04 Wilmer RicciottiProof-irrelevance check for all applications (first...
2008-06-04 Wilmer Ricciottiincomplete irrelevance test commented out
2008-05-30 Enrico TassiCProp hierarchy is there!
2008-05-30 Enrico Tassiirrelevance check half implemented but already impossib...
2008-05-30 Enrico Tassiprod moved under lambda-prolog unification case
2008-05-30 Enrico Tassithanks to the fact that we convert well typed term...
2008-05-30 Enrico Tassiadded a bit more reduction in case Prod v.s. term,...
2008-05-29 Enrico Tassirelevance check partially implemented but bugged since...
2008-05-29 Enrico TassiCProp, since it was defined in CoRN as a Type, is predi...
2008-05-29 Enrico Tassiunused variables removed
2008-05-29 Enrico Tassiref sync check fixed controlling fix/cofix coherence
2008-05-29 Enrico Tassithe type of the match was obtained reducing the outtype
2008-05-27 Enrico Tassismarter lexer needed by lambda-delta that is splitting...
2008-05-26 Enrico Tassinew, more rigid syntax, for auto_params affecting the...
2008-05-26 Enrico TassiUniverse.key was not used to index terms, but was used...
2008-05-26 Enrico Tassiadded comment for zack
2008-05-24 Enrico Tassiorder of goals changes, open ones are preferred to...
2008-05-21 Enrico Tassiminimal implementation of left parameters display
2008-05-19 Claudio Sacerdoti... Here is where we should add relevance checks.
2008-05-19 Claudio Sacerdoti... Bug fixed in computation of leftnos: variables were...
2008-05-19 Claudio Sacerdoti... Code simplification.
2008-05-19 Claudio Sacerdoti... Added cprop <= type constraint.
2008-05-19 Claudio Sacerdoti... We do not need to give cprop a special status yet.
2008-05-19 Claudio Sacerdoti... ...
2008-05-19 Claudio Sacerdoti... CProp dropped in favour of a cprop universe exported...
2008-05-19 Enrico Tassiadded leftno to references f inductive types and constr...
2008-05-19 Enrico Tassiadded aps generation
2008-05-19 Enrico Tassi...
2008-05-19 Enrico Tassirenamed add_le_constraint to add_constraint since it...
2008-05-18 Claudio Sacerdoti... ...
2008-05-18 Claudio Sacerdoti... Bug fixed: when computing the left arguments, I was...
2008-05-18 Enrico Tassirevert last commit, context' -> context (added comment)
2008-05-18 Enrico Tassiusing the right names in the context to check match...
2008-05-18 Claudio Sacerdoti... New missing check implemented: the left parameters...
2008-05-18 Claudio Sacerdoti... This commit avoids cleaning dummy dependent types in...
2008-05-18 Claudio Sacerdoti... Implemented translation of inductive types from the...
2008-05-18 Claudio Sacerdoti... Serious bug fixed: the max of two universes was compute...
2008-05-18 Claudio Sacerdoti... Synch with the paper.
2008-05-18 Claudio Sacerdoti... ...
2008-05-18 Claudio Sacerdoti... Error message improved.
2008-05-18 Claudio Sacerdoti... More effective optimization: avoid introducing already...
2008-05-17 Enrico Tassiimpredicative Set is considered as Prop in the new...
2008-05-17 Claudio Sacerdoti... New check implemented: the sort of each constructor...
next