| 2008-03-31 |
Claudio Sacerdoti... | Automatic generation of elimination and inversion princ... |
commit | commitdiff | tree | snapshot |
| 2008-03-31 |
Claudio Sacerdoti... | Large amount of duplicated code (still in comments... |
commit | commitdiff | tree | snapshot |
| 2008-03-31 |
Claudio Sacerdoti... | 1) Impredicative sort "Set" removed everywhere. |
commit | commitdiff | tree | snapshot |
| 2008-03-31 |
Claudio Sacerdoti... | 1) more sharing everywhere in NCicSubstitution |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | more cases of the type checker honoured, still missing... |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | added is_closed to nCicUtils. |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | moved psubst and list to the new iterators, result... |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | added iterators over NCic terms |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | removed FSF header |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Wilmer Ricciotti | Updated depedencies. |
commit | commitdiff | tree | snapshot |
| 2008-03-27 |
Enrico Tassi | insert comments of old tpechecker |
commit | commitdiff | tree | snapshot |
| 2008-03-26 |
Wilmer Ricciotti | Reorganization of list library (step 1) |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | new are_convertible and head_beta_reduce |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | context for fixpoint body created in the hopefully... |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | ported to the Cic LetIn with explicit type |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | this patch is a shit, the part that fixes the heuristic... |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | fix with m (to be optimized) are rewritten such that... |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | very very interesting hack |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Wilmer Ricciotti | small update |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | argument of type mcu_type always abstracted first |
commit | commitdiff | tree | snapshot |
| 2008-03-25 |
Enrico Tassi | XXX this is the beginning of the metaocaml work XXX |
commit | commitdiff | tree | snapshot |
| 2008-03-23 |
Enrico Tassi | Fsub moved in contribs |
commit | commitdiff | tree | snapshot |
| 2008-03-23 |
Ferruccio Guidi | cicNotationPp: fixed letin syntax (now typeless) |
commit | commitdiff | tree | snapshot |
| 2008-03-22 |
Enrico Tassi | since many stuff is under contrib, we need to ignore... |
commit | commitdiff | tree | snapshot |
| 2008-03-22 |
Enrico Tassi | library_auto moved inside contrib, still not ported... |
commit | commitdiff | tree | snapshot |
| 2008-03-22 |
Enrico Tassi | moved dama/ and dama_didactic/ in contribs/dama/ |
commit | commitdiff | tree | snapshot |
| 2008-03-22 |
Enrico Tassi | freescale moved under contribs. contribs made relocatable |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Claudio Sacerdoti... | New syntax for auto-related tactics and conclude/obtain. |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Claudio Sacerdoti... | Script fixed (it did not compile due to a mistake befor... |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Ferruccio Guidi | Base-2 is not compiling properly and is excluded for now |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | new semantics for 'by t' |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | removed pointless test |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | I believe that auto paramodulation does not try to |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | added library option to auto |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | letins are no more unfolded, we do that by hand |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Enrico Tassi | letin are no longer unfolded thus coercions not propaga... |
commit | commitdiff | tree | snapshot |
| 2008-03-20 |
Claudio Sacerdoti... | End of patch for computation of LetIn types. Now types... |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | Bug: types and terms pushed into the context must be... |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | -debug improved |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | Number notation for Coq is back again, waiting for... |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Claudio Sacerdoti... | Files committed by Enrico (a mistake, I suppose) removed. |
commit | commitdiff | tree | snapshot |
| 2008-03-19 |
Ferruccio Guidi | Procedural : added some missing cases |
commit | commitdiff | tree | snapshot |
| 2008-03-18 |
Ferruccio Guidi | LAMBDA-TYPES: level 2 dependences are now correct,... |
commit | commitdiff | tree | snapshot |
| 2008-03-18 |
Ferruccio Guidi | Procedural : tentative update to the new letin cic... |
commit | commitdiff | tree | snapshot |
| 2008-03-14 |
Claudio Sacerdoti... | Tests enabled again. |
commit | commitdiff | tree | snapshot |
| 2008-03-13 |
Claudio Sacerdoti... | :-( |
commit | commitdiff | tree | snapshot |
| 2008-03-13 |
Claudio Sacerdoti... | New version of freescale: |
commit | commitdiff | tree | snapshot |
| 2008-03-12 |
Claudio Sacerdoti... | Problem solved (was: apply needed an argument to avoid... |
commit | commitdiff | tree | snapshot |
| 2008-03-12 |
Claudio Sacerdoti... | Almost always correct optimization: during unification... |
commit | commitdiff | tree | snapshot |
| 2008-03-12 |
Enrico Tassi | fixed implicit |
commit | commitdiff | tree | snapshot |
| 2008-03-12 |
Andrea Asperti | Nuova dimostrazione riflessiva di le_to_Bertrand. |
commit | commitdiff | tree | snapshot |
| 2008-03-12 |
Enrico Tassi | if -debug is specified do not catch all exceptions |
commit | commitdiff | tree | snapshot |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Enrico Tassi | fixed wrong dependencies in debian package reported... |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | Bad hack to avoid failure of conversion (unfolding... |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | Scripts fixed because of: |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | whd: ~delta=false now controls also zeta-reduction... |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | An unimplemented case of clearbody is now implemented. |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | check_metasenv_consistency: |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | Example query fixed. |
commit | commitdiff | tree | snapshot |
| 2008-03-10 |
Claudio Sacerdoti... | Debugging print removed. |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Claudio Sacerdoti... | Added ad-hoc optimization for check_metasenv_consistenc... |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Claudio Sacerdoti... | Performance improvement: let-ins should always be pushe... |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Claudio Sacerdoti... | Scripts fixed. They were broken since the change to... |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Ferruccio Guidi | LAMBDA-TYPES: some more generation lemmas and some... |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Claudio Sacerdoti... | Potentially (and, at least sometimes, actually) big... |
commit | commitdiff | tree | snapshot |
| 2008-03-09 |
Claudio Sacerdoti... | Redundant check (because of an invariant) removed. |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | * please let the library in shape * |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | fixed |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | skipped freescale and dama_didactic |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | fixed deps |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | reworked freescale stuff to put \m as a left parameter |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | no more assembly/ to skip |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | fix typo |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | added mkdir |
commit | commitdiff | tree | snapshot |
| 2008-03-06 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-03-05 |
Ferruccio Guidi | some corrections and additions |
commit | commitdiff | tree | snapshot |
| 2008-03-05 |
Enrico Tassi | from now on, export MATITA_EXTRACT=true to extract |
commit | commitdiff | tree | snapshot |
| 2008-03-05 |
Enrico Tassi | verbosity increased in case of error |
commit | commitdiff | tree | snapshot |
| 2008-03-04 |
Ferruccio Guidi | components/library: dotdothack removed |
commit | commitdiff | tree | snapshot |
| 2008-03-04 |
Claudio Sacerdoti... | New syntax for patterns. |
commit | commitdiff | tree | snapshot |
| 2008-03-04 |
Claudio Sacerdoti... | prodT ==> prod |
commit | commitdiff | tree | snapshot |
| 2008-03-04 |
Claudio Sacerdoti... | A) New version. |
commit | commitdiff | tree | snapshot |
| 2008-02-29 |
Ferruccio Guidi | we added the classic substitution function |
commit | commitdiff | tree | snapshot |
| 2008-02-28 |
Enrico Tassi | firs attempt to compile with ocamlbuild |
commit | commitdiff | tree | snapshot |
| 2008-02-27 |
Wilmer Ricciotti | the proof of bertrand's conjecture is now complete |
commit | commitdiff | tree | snapshot |
| 2008-02-26 |
Ferruccio Guidi | I added some debugging information |
commit | commitdiff | tree | snapshot |
| 2008-02-26 |
Ferruccio Guidi | added MATITAOPTIONS -onepass as for LAMBDA-TYPES |
commit | commitdiff | tree | snapshot |
| 2008-02-26 |
Ferruccio Guidi | LAMBDA-TYPES: added wf3 (legal context predicate); |
commit | commitdiff | tree | snapshot |
| 2008-02-24 |
Ferruccio Guidi | $(H) added :) |
commit | commitdiff | tree | snapshot |
| 2008-02-24 |
Ferruccio Guidi | LAMBDA-TYPES: dependences calculation improved |
commit | commitdiff | tree | snapshot |
| 2008-02-23 |
Ferruccio Guidi | LAMBDA-TYPES: |
commit | commitdiff | tree | snapshot |
| 2008-02-22 |
Ferruccio Guidi | - added some options to matitadep: -stdout and -exclude |
commit | commitdiff | tree | snapshot |
| 2008-02-22 |
Wilmer Ricciotti | sieve of erathostene (proof of soundness almost done) |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog