| 2008-04-01 |
Enrico Tassi | better check for progress |
tree | commitdiff |
| 2008-04-01 |
Claudio Sacerdoti... | typeof_obj0 implemented |
tree | commitdiff |
| 2008-04-01 |
Claudio Sacerdoti... | 1) added get_checked_indtys that returns the whole... |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | progress made better, still not perfect |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | added to rewrite a check to effectively do something... |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | added some comments, but the samentics of many function... |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | added set_ppterm |
tree | commitdiff |
| 2008-03-31 |
Claudio Sacerdoti... | Automatic generation of elimination and inversion princ... |
tree | commitdiff |
| 2008-03-31 |
Claudio Sacerdoti... | Large amount of duplicated code (still in comments... |
tree | commitdiff |
| 2008-03-31 |
Claudio Sacerdoti... | 1) Impredicative sort "Set" removed everywhere. |
tree | commitdiff |
| 2008-03-31 |
Claudio Sacerdoti... | 1) more sharing everywhere in NCicSubstitution |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | more cases of the type checker honoured, still missing... |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | added is_closed to nCicUtils. |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | moved psubst and list to the new iterators, result... |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | added iterators over NCic terms |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | removed FSF header |
tree | commitdiff |
| 2008-03-27 |
Enrico Tassi | insert comments of old tpechecker |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | new are_convertible and head_beta_reduce |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | context for fixpoint body created in the hopefully... |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | ported to the Cic LetIn with explicit type |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | this patch is a shit, the part that fixes the heuristic... |
tree | commitdiff |
| 2008-03-25 |
Enrico Tassi | XXX this is the beginning of the metaocaml work XXX |
tree | commitdiff |
| 2008-03-23 |
Ferruccio Guidi | cicNotationPp: fixed letin syntax (now typeless) |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-03-20 |
Claudio Sacerdoti... | End of patch for computation of LetIn types. Now types... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | Bug: types and terms pushed into the context must be... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | Number notation for Coq is back again, waiting for... |
tree | commitdiff |
| 2008-03-19 |
Ferruccio Guidi | Procedural : added some missing cases |
tree | commitdiff |
| 2008-03-18 |
Ferruccio Guidi | Procedural : tentative update to the new letin cic... |
tree | commitdiff |
| 2008-03-13 |
Claudio Sacerdoti... | :-( |
tree | commitdiff |
| 2008-03-12 |
Claudio Sacerdoti... | Almost always correct optimization: during unification... |
tree | commitdiff |
| 2008-03-12 |
Enrico Tassi | fixed implicit |
tree | commitdiff |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Bad hack to avoid failure of conversion (unfolding... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | whd: ~delta=false now controls also zeta-reduction... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | An unimplemented case of clearbody is now implemented. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | check_metasenv_consistency: |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Debugging print removed. |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Added ad-hoc optimization for check_metasenv_consistenc... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Performance improvement: let-ins should always be pushe... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Potentially (and, at least sometimes, actually) big... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Redundant check (because of an invariant) removed. |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | fix typo |
tree | commitdiff |
| 2008-03-06 |
Enrico Tassi | added mkdir |
tree | commitdiff |
| 2008-03-05 |
Enrico Tassi | verbosity increased in case of error |
tree | commitdiff |
| 2008-03-04 |
Ferruccio Guidi | components/library: dotdothack removed |
tree | commitdiff |
| 2008-02-26 |
Ferruccio Guidi | I added some debugging information |
tree | commitdiff |
| 2008-02-22 |
Ferruccio Guidi | - added some options to matitadep: -stdout and -exclude |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | A new very simple example for recursive functions.... |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Avoid translating back recursive fixes to the same... |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Avoid application to 0 arguments. |
tree | commitdiff |
| 2008-02-21 |
Claudio Sacerdoti... | Better handling of exceptions. |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | splat_args is now better understood and debugged: we... |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | added small test, fixed some bugs |
tree | commitdiff |
| 2008-02-20 |
Enrico Tassi | many fixed in translation functions |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | snapshot inverse tranformation |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | transformation almost finisced, not tested |
tree | commitdiff |
| 2008-02-19 |
Ferruccio Guidi | now inline "file.ma" is allowed. |
tree | commitdiff |
| 2008-02-19 |
Enrico Tassi | initial steps of convertibility |
tree | commitdiff |
| 2008-02-18 |
Enrico Tassi | some bits of reduction, reusing psubst |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | conversion half inplemented |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | reordered cases |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | reorganization of sources |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | substituion and lifting implemented |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | factorized common components of objects |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | added Local pragma, moved leftno and inductive into... |
tree | commitdiff |
| 2008-02-13 |
Enrico Tassi | added leftno to indtypes, better indentation and comments |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | nCic almost finished |
tree | commitdiff |
| 2008-02-12 |
Enrico Tassi | allow to use "../foo/bar.ma" as a path for the include... |
tree | commitdiff |
| 2008-02-08 |
Claudio Sacerdoti... | Bug fixed in generation of elimination principles of... |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | cic defined (half) |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | reindent |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | oldenv2newenv cache |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | uri and references(uri) |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | uri -> reference (2) |
tree | commitdiff |
| 2008-02-05 |
Enrico Tassi | uri -> reference |
tree | commitdiff |
| 2008-01-31 |
Wilmer Ricciotti | One Obj.magic implemented, trust changed to false. |
tree | commitdiff |
| 2008-01-31 |
Wilmer Ricciotti | Transformation back and forth between old and new repre... |
tree | commitdiff |
| 2008-01-31 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2008-01-31 |
Enrico Tassi | new uri defined |
tree | commitdiff |
| 2008-01-31 |
Enrico Tassi | snapshot] |
tree | commitdiff |
| 2008-01-30 |
Enrico Tassi | added meta for the new kernel |
tree | commitdiff |
| 2008-01-30 |
Enrico Tassi | stub functions to make all compile |
tree | commitdiff |
| 2008-01-30 |
Enrico Tassi | basic organization of the new kernel |
tree | commitdiff |
| 2008-01-22 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-01-14 |
Enrico Tassi | added some doc |
tree | commitdiff |
| 2008-01-14 |
Enrico Tassi | better parsing of the root file |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | added a warning when a file is not compiled cause its... |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | Make does not even try to build files that would be... |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | cache for mtime of files is not polluted with None... |
tree | commitdiff |
| 2008-01-11 |
Enrico Tassi | Make was caching too much, thus some targets were not... |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | Even if the error is not localized, it was not a good... |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | Some terms are not localized from the very beginning :-( |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | One more error localized. But the code is really ugly... |
tree | commitdiff |
| next |
projects / helm.git / history