| 2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the... |
tree | commitdiff |
| 2009-07-13 |
Claudio Sacerdoti... | Coercion hiding implemented. Notes: |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Improved error message. |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
| 2009-06-23 |
Claudio Sacerdoti... | 1) NCicTypechecker.typecheck_obj removed, since it... |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | Good: |
tree | commitdiff |
| 2009-06-18 |
Enrico Tassi | debug pps removed |
tree | commitdiff |
| 2009-06-18 |
Claudio Sacerdoti... | Objects are now used to represent also the tactic status. |
tree | commitdiff |
| 2009-06-17 |
Claudio Sacerdoti... | Initial implementation of statuses using objects in... |
tree | commitdiff |
| 2009-06-16 |
Claudio Sacerdoti... | 1) unification hint now takes NG terms (as it should... |
tree | commitdiff |
| 2009-06-16 |
Claudio Sacerdoti... | FIX OF THE PREVIOUS EXPERIMENTAL COMMIT: |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (by CSC,actuall :-) |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
tree | commitdiff |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-18 |
Claudio Sacerdoti... | 1) order of processing of case branches reverted (to... |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | maxmeta implemented |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | maxmeta function to return the heighest meta used so far |
tree | commitdiff |
| 2009-05-15 |
Enrico Tassi | added patch to not unify any term containing the in_sco... |
tree | commitdiff |
| 2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
tree | commitdiff |
| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
tree | commitdiff |
| 2009-05-11 |
Claudio Sacerdoti... | Bug fixed: the relevance list can be shorted then leftn... |
tree | commitdiff |
| 2009-05-10 |
Claudio Sacerdoti... | - critical bug fixed in NCicSubstitution.lift: |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed: left parameters of constructors were unified... |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed: refinement of mutual recursive definitions... |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed in refinement of inductive types: left parame... |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | The relevance list can be shorter than leftno (when... |
tree | commitdiff |
| 2009-05-06 |
Enrico Tassi | updated comment |
tree | commitdiff |
| 2009-05-05 |
Enrico Tassi | - pretty printer made robust in face of list_nth |
tree | commitdiff |
| 2009-04-29 |
Claudio Sacerdoti... | Refinement of inductive type implemented. |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-14 |
Claudio Sacerdoti... | Trick: the refiner always subst-expands the outtype... |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | ?_OS1 := C[ ?_IN ] |
tree | commitdiff |
| 2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and... |
tree | commitdiff |
| 2009-04-06 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | eta-contraction was made on the wrong term |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | unification: |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created... |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-03-11 |
Enrico Tassi | unification hints with recursive calls do work! |
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-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
tree | commitdiff |
| 2009-02-11 |
Enrico Tassi | some work to refine objs |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | added better debug_pps and add_user_provided_unificatio... |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | lambda case fixed, used to not properly use the expecte... |
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 | make it compile again |
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-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-11 |
Claudio Sacerdoti... | Applications are now processed from left to right. |
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 | 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... | Debugging code removed |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging instructions removed. |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | raise failure instead of uncertain if two terms are... |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Fixes: |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | it works! |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | metas for terms have height 3 |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | loc * lazy string -> (loc * string) lazy |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | disambiguation now returns and takes in input the subst... |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | occurr check fixed |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | more printings |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | do not erase sorts |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | better error messages. sorts are compared using whd |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | Evil case fixed, the coulde should be more readable |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | removed empty lines |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | many bugs fixed |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | better pps |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | - mk_restricted_irl removed, the non-optimized code... |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | more bug fixed (or introduced) |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | delifting a Meta with an IRL w.r.t. another IRL complet... |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | some bug fixed |
tree | commitdiff |
| 2008-10-15 |
Enrico Tassi | subst_meta was missing |
tree | commitdiff |
| 2008-10-14 |
Enrico Tassi | more work |
tree | commitdiff |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported... |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | initial refiner .... |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | NCicReduction.reduce_machine returns a boolean stating... |
tree | commitdiff |
| 2008-10-08 |
Wilmer Ricciotti | Fixed a performance problem with unif_machines and... |
tree | commitdiff |
| 2008-10-06 |
Enrico Tassi | slow example |
tree | commitdiff |
| 2008-10-06 |
Enrico Tassi | 3 nasty bugs fixed: |
tree | commitdiff |
| next |
projects / helm.git / history