| 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 |
| 2007-12-04 |
Enrico Tassi | if parameter type is given, this assert is false |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | Reindented. |
tree | commitdiff |
| 2007-11-30 |
Enrico Tassi | added a way to generate all the utf8 symbols |
tree | commitdiff |
| 2007-11-28 |
Claudio Sacerdoti... | Bug fixed: an unification exception used to escape... |
tree | commitdiff |
| 2007-11-27 |
Claudio Sacerdoti... | Back-ported to camlp5 < 5.00. |
tree | commitdiff |
| 2007-11-26 |
Stefano Zacchiroli | add dump of position information in the lexed file |
tree | commitdiff |
| 2007-11-25 |
Claudio Sacerdoti... | This version of disambiguate.ml implements yet another... |
tree | commitdiff |
| 2007-11-25 |
Claudio Sacerdoti... | Bug fixed: an unification exception used to escape... |
tree | commitdiff |
| 2007-11-23 |
Enrico Tassi | restored the right context used to generate names.... |
tree | commitdiff |
| 2007-11-23 |
Claudio Sacerdoti... | This alternative version of disambiguate.crit2 implemen... |
tree | commitdiff |
| 2007-11-23 |
Enrico Tassi | fast and sound registry lists |
tree | commitdiff |
| 2007-11-19 |
Claudio Sacerdoti... | Bug fixed: local type declarations are not allowed... |
tree | commitdiff |
| 2007-11-17 |
Enrico Tassi | moved to pkg-ocaml-maint |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | compose tactic restore and added nocomposites keyword |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | added -noinnertypes |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | removed prerr_endline |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | removed ugly prerr_endline |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | added ~delta parameter to saturate_term and used it... |
tree | commitdiff |
| 2007-11-14 |
Claudio Sacerdoti... | Bug fixed: yet another case where tys of mutual recursi... |
tree | commitdiff |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
tree | commitdiff |
| 2007-11-13 |
Ferruccio Guidi | - ProofEngineHelpers: namer_of moved to GrafiteEngine |
tree | commitdiff |
| 2007-11-12 |
Ferruccio Guidi | - destruct tactic: automatic simplification in case... |
tree | commitdiff |
| 2007-11-12 |
Enrico Tassi | removed ugly printing |
tree | commitdiff |
| 2007-11-10 |
Claudio Sacerdoti... | a) Detection of existential types now implemented |
tree | commitdiff |
| 2007-11-10 |
Claudio Sacerdoti... | More correct (but still bugged) implementation of type... |
tree | commitdiff |
| 2007-11-10 |
Claudio Sacerdoti... | Dead code removed. |
tree | commitdiff |
| 2007-11-08 |
Claudio Sacerdoti... | Trivial bug fixed in type inference of LetIn source... |
tree | commitdiff |
| 2007-11-08 |
Claudio Sacerdoti... | Arguments of constructors in a case pattern are now... |
tree | commitdiff |
| 2007-11-08 |
Enrico Tassi | please, commit files with debug=false otherwise the... |
tree | commitdiff |
| 2007-11-07 |
Ferruccio Guidi | - bug fix in destruct |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-11-06 |
Claudio Sacerdoti... | cic_acic should be compiled before cic_exportation |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Bug in detection of too polymorphic types partially... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | MutCases that occur in types should be handled with... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Obj.magic are now generated to extract dependently... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Handling of left parameters of constructors/indutive... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Slightly nicer output. |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Filenames are now fully mangled (e.g. matita_nat_nat... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | Type application and abstractions are now exported... |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | New OCaml keyword "val". |
tree | commitdiff |
| 2007-11-05 |
Claudio Sacerdoti... | "f" => "aux" to avoid name clashes |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | The type parameters in an inductive type declaration... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | Type arguments are better uncapitalized. |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | Empty types not in Prop and empty types elimination... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | Empty and singleton type elimination are now handled... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | 1. type definitions of propositions are no longer expor... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | * type definitions that define a new proposition are... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | All exported names are now qualified. This avoids the... |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | All names are now qualified. This avoids the need for... |
tree | commitdiff |
| 2007-11-02 |
Claudio Sacerdoti... | *** Very experimental and not branched *** |
tree | commitdiff |
| 2007-11-02 |
Ferruccio Guidi | - tacticals: new tactical ifs added: uses thens where... |
tree | commitdiff |
| 2007-11-02 |
Claudio Sacerdoti... | Added an hook useful in many situations. |
tree | commitdiff |
| 2007-10-30 |
Ferruccio Guidi | better implementation of if_ |
tree | commitdiff |
| 2007-10-29 |
Ferruccio Guidi | - destruct: core of subst tactic implemented, |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | Pretty-printing of "match ... with" pattern syntax... |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | rebuilt |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | rebuilt |
tree | commitdiff |
| 2007-10-26 |
Claudio Sacerdoti... | Syntax of patterns changed (and not documented yet). |
tree | commitdiff |
| 2007-10-26 |
Claudio Sacerdoti... | Wildcard patterns implemented in case analysis. The... |
tree | commitdiff |
| 2007-10-25 |
Ferruccio Guidi | bug fix in injection e relocate term |
tree | commitdiff |
| next |
projects / helm.git / history