| 2008-06-11 |
Enrico Tassi | meta not considered before in outtype |
tree | commitdiff |
| 2008-06-10 |
Wilmer Ricciotti | relevance check for Match |
tree | commitdiff |
| 2008-06-10 |
Wilmer Ricciotti | Added check of relevance lists for inductive types... |
tree | commitdiff |
| 2008-06-09 |
Claudio Sacerdoti... | It is now possible to use identifiers in place of URI... |
tree | commitdiff |
| 2008-06-09 |
Wilmer Ricciotti | Reverting to the previous version some files which... |
tree | commitdiff |
| 2008-06-09 |
Wilmer Ricciotti | more proof irrelevance |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Bug fixed: wrong default pattern for generalize. |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
tree | commitdiff |
| 2008-06-04 |
Wilmer Ricciotti | Proof-irrelevance check for all applications (first... |
tree | commitdiff |
| 2008-06-04 |
Wilmer Ricciotti | incomplete irrelevance test commented out |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | irrelevance check half implemented but already impossib... |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | prod moved under lambda-prolog unification case |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | thanks to the fact that we convert well typed term... |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | added a bit more reduction in case Prod v.s. term,... |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | relevance check partially implemented but bugged since... |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predi... |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | unused variables removed |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | ref sync check fixed controlling fix/cofix coherence |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | the type of the match was obtained reducing the outtype |
tree | commitdiff |
| 2008-05-27 |
Enrico Tassi | smarter lexer needed by lambda-delta that is splitting... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | Universe.key was not used to index terms, but was used... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | added comment for zack |
tree | commitdiff |
| 2008-05-24 |
Enrico Tassi | order of goals changes, open ones are preferred to... |
tree | commitdiff |
| 2008-05-21 |
Enrico Tassi | minimal implementation of left parameters display |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | Here is where we should add relevance checks. |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | Bug fixed in computation of leftnos: variables were... |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | Code simplification. |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | Added cprop <= type constraint. |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | We do not need to give cprop a special status yet. |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-05-19 |
Claudio Sacerdoti... | CProp dropped in favour of a cprop universe exported... |
tree | commitdiff |
| 2008-05-19 |
Enrico Tassi | added leftno to references f inductive types and constr... |
tree | commitdiff |
| 2008-05-19 |
Enrico Tassi | added aps generation |
tree | commitdiff |
| 2008-05-19 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-19 |
Enrico Tassi | renamed add_le_constraint to add_constraint since it... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Bug fixed: when computing the left arguments, I was... |
tree | commitdiff |
| 2008-05-18 |
Enrico Tassi | revert last commit, context' -> context (added comment) |
tree | commitdiff |
| 2008-05-18 |
Enrico Tassi | using the right names in the context to check match... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | New missing check implemented: the left parameters... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | This commit avoids cleaning dummy dependent types in... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Implemented translation of inductive types from the... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Serious bug fixed: the max of two universes was compute... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Synch with the paper. |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | Error message improved. |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | More effective optimization: avoid introducing already... |
tree | commitdiff |
| 2008-05-17 |
Enrico Tassi | impredicative Set is considered as Prop in the new... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | New check implemented: the sort of each constructor... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Missing check implemented: the sort of each constructor... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | The file bug_universi.ma shows a strage case where... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Missing whd. |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: since circular <= graphs are allowed, added... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: only Type < Type1 was declared. |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed and further code semplification in management... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | The code for universes was not correct in many borderli... |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | ranking reports the lest of univs |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | added new implementation of universes |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | added name_of_uri |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | meta VS meta in alpha_eq honors substitution |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | used ind/coind information in references |
tree | commitdiff |
| 2008-05-16 |
Enrico Tassi | types where compared without lookig at test_eq_only |
tree | commitdiff |
| 2008-05-15 |
Claudio Sacerdoti... | Timings |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | (Approximated) inference of relevance implemented:... |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | First implementation of irrelevance in conversion. |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | New function get_relevance and new (not exported) funct... |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | New function list_forall_default3. 3 euros to the first... |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | Bug fixed in computation of heights: a constant must... |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | Implementation of calculation of heights. |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | Typo fixed. |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | Major code semplification and bugs removed (thanks... |
tree | commitdiff |
| 2008-05-15 |
Andrea Asperti | Removed two args from psubst. |
tree | commitdiff |
| 2008-05-15 |
Enrico Tassi | height of constants properly handled |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | list_iter2_default_value moved to HExtlib. 1 euro to... |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | eat_lambdas and eat_or_subst_lambdas taken out of the... |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | debruijn simplified. It could go in nCicUtils, but... |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | Bug fixed: types were check for conversion in the wrong... |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | We forgot an important check: the declared and expected... |
tree | commitdiff |
| 2008-05-14 |
Enrico Tassi | partial implementation of reduction up to a given height |
tree | commitdiff |
| 2008-05-14 |
Enrico Tassi | fixed error message |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | New checks for well-formedness of metasenvs and substs. |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_... |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | Nicer graph. |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | map_hash moved to HExtlib |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | New function map_hash. |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | Generation of dot file. |
tree | commitdiff |
| 2008-05-14 |
Claudio Sacerdoti... | New licence used uniformly everywhere. |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | One more bug fixed: we tried to perform List.nth on... |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | More exceptions captured. |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Bug fixed in pretty-printing of free Rels. |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Never commit before trying to compile... stupid typo... |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Used old kernel exception in place of brand new one. |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | - is_closed removed from the kernel (it used to make... |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Library factorized out. |
tree | commitdiff |
| 2008-05-13 |
Enrico Tassi | wrong test equality only fixed |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Type of conjecture and subst_entry made uniform. |
tree | commitdiff |
| 2008-05-13 |
Enrico Tassi | convertibility was taking a metasenv but not using it |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Added boolean "is_inductive" to NReference.Ind |
tree | commitdiff |
| next |
projects / helm.git / history