| 2008-07-22 |
Ferruccio Guidi | matitadep: we now handle the inline of an uri, we remov... |
tree | commitdiff |
| 2008-07-22 |
Ferruccio Guidi | transcript: now we can generate procedural output |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | Error message improved. |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | Rendering of \infrule improved. |
tree | commitdiff |
| 2008-07-21 |
Ferruccio Guidi | we implemented the support for generating ma files... |
tree | commitdiff |
| 2008-07-21 |
Enrico Tassi | avoid empty hvbox |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | better metavariable context |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | metavariable context has a separator now |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | exception inside regex callback not re-raised if equal... |
tree | commitdiff |
| 2008-07-17 |
Claudio Sacerdoti... | Bugs fixed: |
tree | commitdiff |
| 2008-07-16 |
Ferruccio Guidi | Procedural: some comments added in the generated script |
tree | commitdiff |
| 2008-07-16 |
Enrico Tassi | notations for lists adds some breaking points |
tree | commitdiff |
| 2008-07-15 |
Ferruccio Guidi | cic2acic: new function acic_term_of_cic_term |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i |
tree | commitdiff |
| 2008-07-14 |
Ferruccio Guidi | lambda-delta: we added the support for position indexes... |
tree | commitdiff |
| 2008-07-14 |
Ferruccio Guidi | Procedural: we added the support for rendering definiti... |
tree | commitdiff |
| 2008-07-13 |
Ferruccio Guidi | Procedural: we added the support for theorem flavours... |
tree | commitdiff |
| 2008-07-13 |
Ferruccio Guidi | cicUtil : we added a context to is_sober... |
tree | commitdiff |
| 2008-07-12 |
Ferruccio Guidi | Procedural: bug fix in the procedural rendering of... |
tree | commitdiff |
| 2008-07-12 |
Ferruccio Guidi | librarian: retrieval of buildable files speeded up... |
tree | commitdiff |
| 2008-07-12 |
Claudio Sacerdoti... | New feature/bug fixed (hopefully): it is now possible... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | Exists is no longer an ad-hoc notation hard-coded in... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | Added new ternary layout \infrule premises conclusion... |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | fixed regression in casting an argument to funclass... |
tree | commitdiff |
| 2008-07-09 |
Ferruccio Guidi | some bug fixes |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | tab -> ' ' |
tree | commitdiff |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - we replaced a normalize with a whd in the classificat... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - Procedural: bug fix in rendering the application... |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-07-02 |
Wilmer Ricciotti | Fixed a bug which prevented mutually recursive definiti... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | calculation of the sort user to choose the rewriting... |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | better, reparsable, notation |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | missing file added |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | add \\ in front of tex macros |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane... |
tree | commitdiff |
| 2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | - partial implementation of pattern for case documented |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation fixed to be NON associative by default |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
tree | commitdiff |
| 2008-06-19 |
Ferruccio Guidi | - Procedural: we now check that an eliminator opens... |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-06-18 |
Enrico Tassi | initial support for notation that specifies the precede... |
tree | commitdiff |
| 2008-06-17 |
Enrico Tassi | reordering of lexicon status partially avoided to make... |
tree | commitdiff |
| 2008-06-13 |
Wilmer Ricciotti | final relevance check |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | replace assert false with AssertFailure |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | print the name not found in the env |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history