| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent products in inductive types arities... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | This commit avoids cleaning dummy dependent types in... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Implemented translation of inductive types from the... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Serious bug fixed: the max of two universes was compute... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Synch with the paper. |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | Error message improved. |
commit | commitdiff | tree | snapshot |
| 2008-05-18 |
Claudio Sacerdoti... | More effective optimization: avoid introducing already... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Enrico Tassi | impredicative Set is considered as Prop in the new... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | New check implemented: the sort of each constructor... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | Missing check implemented: the sort of each constructor... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | The file bug_universi.ma shows a strage case where... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | Missing whd. |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: since circular <= graphs are allowed, added... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: only Type < Type1 was declared. |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed and further code semplification in management... |
commit | commitdiff | tree | snapshot |
| 2008-05-17 |
Claudio Sacerdoti... | The code for universes was not correct in many borderli... |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | ranking reports the lest of univs |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | added new implementation of universes |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | added name_of_uri |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | meta VS meta in alpha_eq honors substitution |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | used ind/coind information in references |
commit | commitdiff | tree | snapshot |
| 2008-05-16 |
Enrico Tassi | types where compared without lookig at test_eq_only |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Claudio Sacerdoti... | Timings |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | (Approximated) inference of relevance implemented:... |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | First implementation of irrelevance in conversion. |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | New function get_relevance and new (not exported) funct... |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | New function list_forall_default3. 3 euros to the first... |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | Bug fixed in computation of heights: a constant must... |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | Implementation of calculation of heights. |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | Typo fixed. |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | Major code semplification and bugs removed (thanks... |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Andrea Asperti | Removed two args from psubst. |
commit | commitdiff | tree | snapshot |
| 2008-05-15 |
Enrico Tassi | height of constants properly handled |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | list_iter2_default_value moved to HExtlib. 1 euro to... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | eat_lambdas and eat_or_subst_lambdas taken out of the... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | debruijn simplified. It could go in nCicUtils, but... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | Bug fixed: types were check for conversion in the wrong... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | We forgot an important check: the declared and expected... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Enrico Tassi | partial implementation of reduction up to a given height |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Enrico Tassi | fixed error message |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | New checks for well-formedness of metasenvs and substs. |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_... |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | Nicer graph. |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | map_hash moved to HExtlib |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | New function map_hash. |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | Generation of dot file. |
commit | commitdiff | tree | snapshot |
| 2008-05-14 |
Claudio Sacerdoti... | New licence used uniformly everywhere. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Ferruccio Guidi | we added a link to lambda-delta home page in the hope... |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | One more bug fixed: we tried to perform List.nth on... |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | More exceptions captured. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Bug fixed in pretty-printing of free Rels. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Never commit before trying to compile... stupid typo... |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Used old kernel exception in place of brand new one. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | - is_closed removed from the kernel (it used to make... |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Library factorized out. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Enrico Tassi | wrong test equality only fixed |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Type of conjecture and subst_entry made uniform. |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Enrico Tassi | convertibility was taking a metasenv but not using it |
commit | commitdiff | tree | snapshot |
| 2008-05-13 |
Claudio Sacerdoti... | Added boolean "is_inductive" to NReference.Ind |
commit | commitdiff | tree | snapshot |
| 2008-05-12 |
Claudio Sacerdoti... | trust is always false by default |
commit | commitdiff | tree | snapshot |
| 2008-05-12 |
Claudio Sacerdoti... | trust implemented, but in the nCicTypeChecker! |
commit | commitdiff | tree | snapshot |
| 2008-05-12 |
Claudio Sacerdoti... | New implementation of CicEnvironment: |
commit | commitdiff | tree | snapshot |
| 2008-05-12 |
Enrico Tassi | height is stored in the reference, no need to fetch... |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | fixed english |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | valid xml |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | released 0.5.0 |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-10 |
Enrico Tassi | some files orphaned |
commit | commitdiff | tree | snapshot |
| 2008-05-09 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-09 |
Enrico Tassi | a missing prime |
commit | commitdiff | tree | snapshot |
| 2008-05-09 |
Claudio Sacerdoti... | Bug fixed: the domain of a LetRec was only made by... |
commit | commitdiff | tree | snapshot |
| 2008-05-07 |
Claudio Sacerdoti... | Update after some more bug fixing. |
commit | commitdiff | tree | snapshot |
| 2008-05-07 |
Claudio Sacerdoti... | Partially reverted bad merge by Enrico that re-introduc... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Claudio Sacerdoti... | More bugs fixed. |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | get_check_fix and cofix unified, bug regarding debruijn... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | get_checked_indtys can take a constructor reference |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | added mk_cofix |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | let corec |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | CoFix cache implemented |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | fix_left_in_constr still broken, ask enrico |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | guarded_by_constructors implemented, some cleanup here... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | removed dead code |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions... |
commit | commitdiff | tree | snapshot |
| 2008-05-03 |
Claudio Sacerdoti... | Broken XML files either fixed or removed. |
commit | commitdiff | tree | snapshot |
| 2008-05-02 |
Wilmer Ricciotti | Some destruct tactics got broken after last update... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | More precise classification of failures. |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | List of all URIS comprising: |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | More options can now be set at the beginning of the... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Last (???) bug about variables with bodies fixed: we... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Another case where the presence of variables with bodie... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Enrico Tassi | tagging 0.5.0-rc1 |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Bug fixed: application without arguments generated... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | New bug found. |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog