2009-03-30 |
Enrico Tassi | ... |
tree | commitdiff |
2009-03-27 |
Enrico Tassi | more comments |
tree | commitdiff |
2009-03-27 |
Enrico Tassi | exec and distribute implemented |
tree | commitdiff |
2009-03-26 |
Enrico Tassi | new apply almost there |
tree | commitdiff |
2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
2009-03-16 |
Andrea Asperti | New parameters for applyS: 10 20. |
tree | commitdiff |
2009-03-11 |
Ferruccio Guidi | Procedural: id tactics are not counted, ie they are... |
tree | commitdiff |
2009-03-11 |
Ferruccio Guidi | bug fix + better obj flavour guessing via inner sorts |
tree | commitdiff |
2009-03-11 |
Ferruccio Guidi | the level 1 reconstruction procedure is now in Procedural1 |
tree | commitdiff |
2009-03-11 |
Ferruccio Guidi | .... |
tree | commitdiff |
2009-03-11 |
Ferruccio Guidi | new dependences |
tree | commitdiff |
2009-03-11 |
Enrico Tassi | unification hints with recursive calls do work! |
tree | commitdiff |
2009-03-11 |
Enrico Tassi | added margin option to the pp |
tree | commitdiff |
2009-03-10 |
Enrico Tassi | unificatiom hints with premises |
tree | commitdiff |
2009-03-10 |
Enrico Tassi | unification hints almost ready |
tree | commitdiff |
2009-03-10 |
Andrea Asperti | A version of applyS with bounded iterations of given_cl... |
tree | commitdiff |
2009-03-10 |
Andrea Asperti | Removed the context from the metasenv to avoid trivial... |
tree | commitdiff |
2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
tree | commitdiff |
2009-03-02 |
Ferruccio Guidi | cicInspect: node count fixed |
tree | commitdiff |
2009-02-26 |
Ferruccio Guidi | cicInspect: now we can choose not to count the Cic... |
tree | commitdiff |
2009-02-25 |
Ferruccio Guidi | ProceduralTeX completed and tested on the terms given... |
tree | commitdiff |
2009-02-21 |
Ferruccio Guidi | New module for TeX rendering of procedural input/output |
tree | commitdiff |
2009-02-20 |
Enrico Tassi | ... |
tree | commitdiff |
2009-02-17 |
Ferruccio Guidi | - Coq/preamble: missing alias added |
tree | commitdiff |
2009-02-15 |
Enrico Tassi | commented some printings |
tree | commitdiff |
2009-02-12 |
Andrea Asperti | errata corrige. |
tree | commitdiff |
2009-02-12 |
Andrea Asperti | Fixed a problem of lifting. |
tree | commitdiff |
2009-02-11 |
Enrico Tassi | some work to refine objs |
tree | commitdiff |
2009-02-05 |
Enrico Tassi | a non necessary but morally required change. The matche... |
tree | commitdiff |
2009-02-03 |
Enrico Tassi | case tactic first tries with a simple outtype and then... |
tree | commitdiff |
2009-02-02 |
Enrico Tassi | CicTypeChecker.typecheck now takes an additional parameter: |
tree | commitdiff |
2009-01-30 |
Enrico Tassi | fix convertibility in case of application test_eq_only... |
tree | commitdiff |
2009-01-29 |
Enrico Tassi | application arguments are compared with test_eq_only... |
tree | commitdiff |
2009-01-26 |
Enrico Tassi | maction layout added to notation |
tree | commitdiff |
2009-01-26 |
Enrico Tassi | we were generating a name for the main fix twice |
tree | commitdiff |
2009-01-26 |
Enrico Tassi | added a number to identical error messages to ease... |
tree | commitdiff |
2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many... |
tree | commitdiff |
2009-01-16 |
Enrico Tassi | ceommented out metasenv |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | if the user attempts to insert a duplicate coercions... |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | unvariant also for coercions to funclass |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | - name mangling changed, added __ to separate additiona... |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | no more universe inconsistency printed to stderr |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | coercions that are marked as variant are unfolded when... |
tree | commitdiff |
2009-01-15 |
Enrico Tassi | Coercions graph is printed between real types and not... |
tree | commitdiff |
2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
2009-01-08 |
Enrico Tassi | more composites to make all happy! |
tree | commitdiff |
2009-01-06 |
Enrico Tassi | coercions reordering implemented |
tree | commitdiff |
2009-01-05 |
Enrico Tassi | removing (only from the interface) functions related... |
tree | commitdiff |
2008-12-24 |
Enrico Tassi | bug fixed, all convertible was called without a metasenv |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | more pps |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | type3 |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | ranking hopefully fixed |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | better pps |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | handles bad Appl |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | added better debug_pps and add_user_provided_unificatio... |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | ... |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | added unification hint |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | unification hint |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | lambda case fixed, used to not properly use the expecte... |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | added 'unification hint command to add a term to the... |
tree | commitdiff |
2008-12-19 |
Enrico Tassi | identity coercions are not really inserted, just used... |
tree | commitdiff |
2008-12-18 |
Claudio Sacerdoti... | Stupid bug fixed: checkin the type in place of the... |
tree | commitdiff |
2008-12-18 |
Claudio Sacerdoti... | New disambiguation commented out. |
tree | commitdiff |
2008-12-18 |
Claudio Sacerdoti... | Now it compiles again. |
tree | commitdiff |
2008-12-18 |
Claudio Sacerdoti... | Refinement of axioms fixed. We did not check that the... |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | previous change was causing divergence |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | hints work better now |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | hints attached |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | removed debug code |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | fixed a bug, it used to report o wrong is_normal bit... |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | make it compile again |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | wrap object_not_found |
tree | commitdiff |
2008-12-16 |
Enrico Tassi | move the printing in the right place |
tree | commitdiff |
2008-12-15 |
Enrico Tassi | dep.opt regenerated |
tree | commitdiff |
2008-12-15 |
Enrico Tassi | added unification hints |
tree | commitdiff |
2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
tree | commitdiff |
2008-12-15 |
Enrico Tassi | To check if a term is type, do a whd of its sort before... |
tree | commitdiff |
2008-12-15 |
Enrico Tassi | aded some whd, you should be able to declare something... |
tree | commitdiff |
2008-12-14 |
Claudio Sacerdoti... | The library is no longer automatically used during... |
tree | commitdiff |
2008-12-14 |
Enrico Tassi | eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg... |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | added some hardcoded universes, needed to typecheck... |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | added some messages |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | added empty_db, usefull to avoid translating all old... |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are... |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
tree | commitdiff |
2008-12-12 |
Enrico Tassi | pattern matching over Ast.Case simplified: |
tree | commitdiff |
2008-12-11 |
Claudio Sacerdoti... | Applications are now processed from left to right. |
tree | commitdiff |
2008-12-11 |
Enrico Tassi | support for mathml mpadded tag added (allows to overlap... |
tree | commitdiff |
2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe... |
tree | commitdiff |
2008-12-09 |
Enrico Tassi | raise uncertain when a sort is not a sort but may be... |
tree | commitdiff |
2008-12-09 |
Enrico Tassi | better coercions indexing and lookup |
tree | commitdiff |
2008-12-09 |
Enrico Tassi | better max function (instead of @) for combining universes |
tree | commitdiff |
2008-12-09 |
Enrico Tassi | saturate was not returning the correct (saturated)... |
tree | commitdiff |
2008-12-07 |
Claudio Sacerdoti... | Bug fixed: every time we form a Prod, we must typecheck... |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Added new syntax Type[n] where n is a number. |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Debugging code removed |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Debugging instructions removed. |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
next |