]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
basic topologies are trivially o-basic topologies
[helm.git] / helm / software / components /
2009-01-15 Enrico Tassiif the user attempts to insert a duplicate coercions...
2009-01-15 Enrico Tassiunvariant also for coercions to funclass
2009-01-15 Enrico Tassi- name mangling changed, added __ to separate additiona...
2009-01-15 Enrico Tassino more universe inconsistency printed to stderr
2009-01-15 Enrico Tassicoercions that are marked as variant are unfolded when...
2009-01-15 Enrico TassiCoercions graph is printed between real types and not...
2009-01-13 Enrico Tassimany changes regarding coercions:
2009-01-08 Enrico Tassimore composites to make all happy!
2009-01-06 Enrico Tassicoercions reordering implemented
2009-01-05 Enrico Tassiremoving (only from the interface) functions related...
2008-12-24 Enrico Tassibug fixed, all convertible was called without a metasenv
2008-12-19 Enrico Tassimore pps
2008-12-19 Enrico Tassitype3
2008-12-19 Enrico Tassiranking hopefully fixed
2008-12-19 Enrico Tassibetter pps
2008-12-19 Enrico Tassihandles bad Appl
2008-12-19 Enrico Tassiadded better debug_pps and add_user_provided_unificatio...
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassiadded unification hint
2008-12-19 Enrico Tassiunification hint
2008-12-19 Enrico Tassilambda case fixed, used to not properly use the expecte...
2008-12-19 Enrico Tassiadded 'unification hint command to add a term to the...
2008-12-19 Enrico Tassiidentity coercions are not really inserted, just used...
2008-12-18 Claudio Sacerdoti... Stupid bug fixed: checkin the type in place of the...
2008-12-18 Claudio Sacerdoti... New disambiguation commented out.
2008-12-18 Claudio Sacerdoti... Now it compiles again.
2008-12-18 Claudio Sacerdoti... Refinement of axioms fixed. We did not check that the...
2008-12-16 Enrico Tassiprevious change was causing divergence
2008-12-16 Enrico Tassihints work better now
2008-12-16 Enrico Tassihints attached
2008-12-16 Enrico Tassiremoved debug code
2008-12-16 Enrico Tassifixed a bug, it used to report o wrong is_normal bit...
2008-12-16 Enrico Tassimake it compile again
2008-12-16 Enrico Tassiwrap object_not_found
2008-12-16 Enrico Tassimove the printing in the right place
2008-12-15 Enrico Tassidep.opt regenerated
2008-12-15 Enrico Tassiadded unification hints
2008-12-15 Wilmer RicciottiFirst attempt to implement unification hints.
2008-12-15 Enrico TassiTo check if a term is type, do a whd of its sort before...
2008-12-15 Enrico Tassiaded some whd, you should be able to declare something...
2008-12-14 Claudio Sacerdoti... The library is no longer automatically used during...
2008-12-14 Enrico Tassieureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg...
2008-12-12 Enrico Tassiadded some hardcoded universes, needed to typecheck...
2008-12-12 Enrico Tassiadded some messages
2008-12-12 Enrico Tassiadded empty_db, usefull to avoid translating all old...
2008-12-12 Enrico Tassiuse new function to clear caches so that objects are...
2008-12-12 Enrico Tassibetter error message, functions to clear various caches...
2008-12-12 Enrico Tassipattern matching over Ast.Case simplified:
2008-12-11 Claudio Sacerdoti... Applications are now processed from left to right.
2008-12-11 Enrico Tassisupport for mathml mpadded tag added (allows to overlap...
2008-12-09 Enrico Tassinew disambiguatio attached with the right universe...
2008-12-09 Enrico Tassiraise uncertain when a sort is not a sort but may be...
2008-12-09 Enrico Tassibetter coercions indexing and lookup
2008-12-09 Enrico Tassibetter max function (instead of @) for combining universes
2008-12-09 Enrico Tassisaturate was not returning the correct (saturated)...
2008-12-07 Claudio Sacerdoti... Bug fixed: every time we form a Prod, we must typecheck...
2008-12-05 Claudio Sacerdoti... Added new syntax Type[n] where n is a number.
2008-12-05 Claudio Sacerdoti... Debugging code removed.
2008-12-05 Claudio Sacerdoti... Debugging code removed
2008-12-05 Claudio Sacerdoti... Debugging instructions removed.
2008-12-05 Claudio Sacerdoti... Useless code removed.
2008-12-05 Claudio Sacerdoti... Useless code removed.
2008-12-05 Claudio Sacerdoti... Useless code removed.
2008-12-05 Enrico Tassia few missing ~subst added to whd
2008-12-05 Enrico Tassicoercions are there, but not heavily tested
2008-12-05 Enrico Tassiif todo_dom was [] disambiguation was performed twice
2008-12-05 Enrico Tassistill commented, but benchmarks the new/old disambiguti...
2008-12-05 Enrico Tassidisambiguation takes ~mk_localization_tbl and not ...
2008-12-05 Enrico Tassiraise failure instead of uncertain if two terms are...
2008-12-04 Enrico TassiFixes:
2008-12-04 Enrico Tassihousekeeping:
2008-12-04 Enrico TassiBug fixed: pretty-printing of aliases when the OK butto...
2008-12-03 Claudio Sacerdoti... The aliases and multi_aliases in the lexicon status...
2008-12-01 Claudio Sacerdoti... rt.op and check.opt removed from Makefile
2008-11-30 Ferruccio Guidilambda-delta/toplevel: improved transformation from...
2008-11-28 Ferruccio GuidicicDischarge: final fixup. Now correctly processes...
2008-11-28 Ferruccio Guiding_disambiguation ng_kernel ng_refiner disambiguation...
2008-11-28 Enrico Tassiit works!
2008-11-28 Enrico Tassinew disambiguator almost attached
2008-11-28 Enrico Tassi\forall x:?. and \forall x. both generate a meta for...
2008-11-28 Enrico Tassimetas for terms have height 3
2008-11-27 Claudio Sacerdoti... ...
2008-11-27 Claudio Sacerdoti... ...
2008-11-27 Claudio Sacerdoti... ...
2008-11-27 Enrico TassiNew modules stack:
2008-11-27 Enrico Tassicic_disambiguation splitted into disambiguation and...
2008-11-27 Enrico Tassidisambiguate.ml splitted into disambiguate.ml and cicDi...
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator
2008-11-27 Enrico Tassinew kernel is compiled since the META of grafite_parser...
2008-11-27 Enrico Tassi...
2008-11-27 Enrico Tassinotation now digests Cic.Cast, not sure the precedence...
2008-11-27 Enrico Tassidisambiguation should not fail if the new refiner fails
2008-11-26 Enrico Tassi...
2008-11-26 Enrico TassiRe-added exception, just for now (debugging).
2008-11-26 Enrico Tassialmost done
2008-11-26 Enrico Tassidisambiguation even more abstracted
2008-11-25 Ferruccio GuidicicUtil: we moved here pp_term from proceduralHelpers
2008-11-21 Enrico Tassi...
2008-11-21 Enrico Tassione more lazy/loc
2008-11-21 Enrico Tassiaccording to camlp5 sources, the dummy loc should be...
next