| 2009-07-31 |
Claudio Sacerdoti... | Pp fixed in order to obtain read-back. |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | "..." -> "\ldots" for implicit vectors |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | Introduction of vectors of implicit (only for NG). |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Serious bug fixed: because of lazy evaluation of !requi... |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | 1) The NG kernel now accepts only usage of declared... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | 1) added a function to retrieve all the universes curre... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Metavariable case in does_not_occur (hence weakly/stric... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Missing case for Match implemented. |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | weakly/strictly positive checks relaxed to allow metava... |
tree | commitdiff |
| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | Bug fixed: one uri was not refreshed, causing divergenc... |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-06-23 |
Enrico Tassi | undo/serialization for universes implemented |
tree | commitdiff |
| 2009-06-23 |
Claudio Sacerdoti... | Debugging prerr_endlines removed. |
tree | commitdiff |
| 2009-06-23 |
Claudio Sacerdoti... | 1) NCicTypechecker.typecheck_obj removed, since it... |
tree | commitdiff |
| 2009-06-23 |
Claudio Sacerdoti... | - Bug fixed: removed URIs were not removed from the... |
tree | commitdiff |
| 2009-06-21 |
Ferruccio Guidi | - cicNotationPp: bugfix in record syntax |
tree | commitdiff |
| 2009-06-20 |
Claudio Sacerdoti... | Debugging |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | Invert dependencies between baseuris (files) are now... |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | Bug fixed: refreshing of uris for the db. |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | The global db is now updated during decompilation. |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | Persistent db (to lookup names in the library) ineffici... |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | NG decompilation is now activated. However, it is calle... |
tree | commitdiff |
| 2009-06-19 |
Claudio Sacerdoti... | Good: |
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... | 1) NCicLibrary (which is untrusted) moved after NCicUnt... |
tree | commitdiff |
| 2009-06-16 |
Claudio Sacerdoti... | Implementation of existential type improved (more stric... |
tree | commitdiff |
| 2009-06-16 |
Claudio Sacerdoti... | FIX OF THE PREVIOUS EXPERIMENTAL COMMIT: |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (part B, by CSC :-): |
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-06-05 |
denes | Fix : wrong exception was catch in apply_subst |
tree | commitdiff |
| 2009-06-05 |
Claudio Sacerdoti... | The kernel _must_ check the correctness of the height... |
tree | commitdiff |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
tree | commitdiff |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | removed useless function |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | alpha_eq exported |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | alpha_eq defined and exported |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | efficiency improvement (buffers are now used everywhere) |
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... | ppsubst commented out in ppobj |
tree | commitdiff |
| 2009-05-11 |
Claudio Sacerdoti... | Buffers are now used everywhere for speed-up. |
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... | The relevance list can be shorter than leftno (when... |
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-26 |
Claudio Sacerdoti... | The backward compatible management of aliases for NG... |
tree | commitdiff |
| 2009-04-25 |
Claudio Sacerdoti... | Lookup_in_library implemented for new objects. Basicall... |
tree | commitdiff |
| 2009-04-25 |
Claudio Sacerdoti... | Better error message. |
tree | commitdiff |
| 2009-04-24 |
Claudio Sacerdoti... | Quick&dirty implementation of neqd: |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-10 |
Claudio Sacerdoti... | The sequent viewer now considers the context to render... |
tree | commitdiff |
| 2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and... |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | added tentative elim |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | removed spurious " |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-03-11 |
Ferruccio Guidi | new dependences |
tree | commitdiff |
| 2009-03-11 |
Enrico Tassi | added margin option to the pp |
tree | commitdiff |
| 2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
tree | commitdiff |
| 2009-02-17 |
Ferruccio Guidi | - Coq/preamble: missing alias added |
tree | commitdiff |
| 2009-02-11 |
Enrico Tassi | some work to refine objs |
tree | commitdiff |
| 2009-01-30 |
Enrico Tassi | fix convertibility in case of application test_eq_only... |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | better pps |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | handles bad Appl |
tree | commitdiff |
| 2008-12-16 |
Enrico Tassi | previous change was causing divergence |
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 | wrap object_not_found |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | better max function (instead of @) for combining universes |
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-04 |
Enrico Tassi | Fixes: |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached |
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-10-27 |
Enrico Tassi | metasenv passed to get_relevance, Metas that stand... |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | _ in place of unused variables |
tree | commitdiff |
| 2008-10-27 |
Enrico Tassi | Implicit annotationas are now printed |
tree | commitdiff |
| 2008-10-21 |
Enrico Tassi | psubst for metas fixed again |
tree | commitdiff |
| 2008-10-20 |
Enrico Tassi | ... |
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 | bug in psubst fixed inside local context in Irl form |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | ppmetasenv & subst added |
tree | commitdiff |
| 2008-10-13 |
Enrico Tassi | NCicReduction.reduce_machine returns a boolean stating... |
tree | commitdiff |
| 2008-10-03 |
Enrico Tassi | - NCicPp.ppterm applies the substitution |
tree | commitdiff |
| 2008-10-03 |
Enrico Tassi | the iterator was wrongly processing the application |
tree | commitdiff |
| 2008-10-03 |
Wilmer Ricciotti | Final implementation of proof irrelevant conversion... |
tree | commitdiff |
| 2008-10-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-10-02 |
Enrico Tassi | we can test the unification algorithm! |
tree | commitdiff |
| next |
projects / helm.git / history