2009-10-04 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-10-04 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-10-04 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | hints fixed |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | fixed bug in coercion application, input/output swapped... |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | if the query has a completely flexible side, the empty... |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | hints input is cleared from projection redexes |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | projections redex (proj (mk_foo ...)) where mk_foo |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Enrico Tassi | better nlet rec boxing |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Claudio Sacerdoti... | Wrong context (again!) |
commit | commitdiff | tree | snapshot |
2009-10-02 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Ferruccio Guidi | better static html pages, now they are generted in... |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | - delift_type_wrt_term fixed in many ways |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | fixed the type of tactic_term, attributes were useless |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | instantiate merges tags |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | added sortification for (? args), untested code |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | sortification simplified |
commit | commitdiff | tree | snapshot |
2009-10-01 |
Enrico Tassi | fixed off-by-one |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Claudio Sacerdoti... | With this hint, it diverges. |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Enrico Tassi | rewritten instantiate code |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Claudio Sacerdoti... | Better (but still broken) fix for the case ?sort vs... |
commit | commitdiff | tree | snapshot |
2009-09-30 |
Claudio Sacerdoti... | The term contains dummy.conv that was searched over... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | 1) improved (???) debugging, with |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | Re-indentiation |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Enrico Tassi | ugly coerc db print |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | The unification does not longer use the refiner (urrah!) |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Enrico Tassi | more virtuals |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | It does not work recursively... |
commit | commitdiff | tree | snapshot |
2009-09-29 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Enrico Tassi | non ho resistito! |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Enrico Tassi | - fixed bug in coercion application, input/output swapp... |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Enrico Tassi | 2 lift related bugs fixed! |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Enrico Tassi | better debug pp |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Claudio Sacerdoti... | Experiment... |
commit | commitdiff | tree | snapshot |
2009-09-28 |
Claudio Sacerdoti... | Experiment... |
commit | commitdiff | tree | snapshot |
2009-09-27 |
Enrico Tassi | Type printed as such, CProp printed as such |
commit | commitdiff | tree | snapshot |
2009-09-27 |
Enrico Tassi | fixpoint have attributes for pragma (i.e. they can... |
commit | commitdiff | tree | snapshot |
2009-09-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-25 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | multi screenshot |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ncheck works in the current ctx |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-24 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | more on screenshot |
commit | commitdiff | tree | snapshot |
2009-09-23 |
Enrico Tassi | new macro screenshot |
commit | commitdiff | tree | snapshot |
2009-09-22 |
Ferruccio Guidi | we improved the stylesheets and we generated the static... |
commit | commitdiff | tree | snapshot |
2009-09-22 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Ferruccio Guidi | xml: bug fix |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Ferruccio Guidi | xml: first ld to xml stylesheets |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | new tactics by CSC |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call... |
commit | commitdiff | tree | snapshot |
2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
commit | commitdiff | tree | snapshot |
2009-09-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Ferruccio Guidi | we start version 0.8.1 by replacing the abstract layer... |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Enrico Tassi | one more exception printed |
commit | commitdiff | tree | snapshot |
2009-09-17 |
Enrico Tassi | more work for igft |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Enrico Tassi | more notation for topologies, and some prentheses that... |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Enrico Tassi | some more work... |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Claudio Sacerdoti... | New interesting coercion. |
commit | commitdiff | tree | snapshot |
2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types... |
commit | commitdiff | tree | snapshot |
2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries. |
commit | commitdiff | tree | snapshot |
2009-09-15 |
Ferruccio Guidi | some renaming. final commit for version 0.8.0 |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Enrico Tassi | fixed coercion mechanism w.r.t. undo/require |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | Slightly simplied status code. |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | Simplest typing for status records. |
commit | commitdiff | tree | snapshot |
2009-09-14 |
Claudio Sacerdoti... | New tactics ncut and nlapply. |
commit | commitdiff | tree | snapshot |
2009-09-13 |
Enrico Tassi | a nice bug in meta handling is not visible... brr... |
commit | commitdiff | tree | snapshot |
2009-09-13 |
Enrico Tassi | some more letters |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | constructor accepts the arguments of the constructor... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new tactic constructor: @[n] |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new syntax |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | let rec/corec and co/inductive are not printed! |
commit | commitdiff | tree | snapshot |
2009-09-11 |
Enrico Tassi | new macro ncheck. fixed term2pres for Inductive and... |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | ok, but slow on includes |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | nice hints |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | maledetto il \sub di CSC |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | it starts to work |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | nice notation for hints! |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | allow @{ ... } as the identifier of the letin |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | to me, the problem: |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Ferruccio Guidi | some interfaces improved |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | more stuff fixed |
commit | commitdiff | tree | snapshot |
2009-09-10 |
Enrico Tassi | the refiner was not checking that the resulting type |
commit | commitdiff | tree | snapshot |
next |