| 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 |
| 2007-10-25 |
Claudio Sacerdoti... | Ooops. In previous commit I forgot to subtract the... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: case analysis where a case had not the expec... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase considering a wrong number of... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase with missing or exceeding cases... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | 1. More localization: interpretation errors are now... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Recently introduced bug fixed: error localization was... |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | bug fix in injection: we have to recur on the generated... |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | we revisited the implementation of the destruct tactic... |
tree | commitdiff |
| 2007-10-24 |
Claudio Sacerdoti... | Debugging code improved. |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | - new function for general relocation of local referenc... |
tree | commitdiff |
| 2007-10-16 |
Enrico Tassi | fixed make opt |
tree | commitdiff |
| 2007-10-16 |
Claudio Sacerdoti... | DOS-style CR+LF added to the blanks list. |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-10-11 |
Claudio Sacerdoti... | Old inversion bug fixed: it used to work only on the... |
tree | commitdiff |
| 2007-10-09 |
Enrico Tassi | added patch to allow i,j,k: skip and *: skip |
tree | commitdiff |
| 2007-09-23 |
Ferruccio Guidi | we chmod the created directories to override the umask... |
tree | commitdiff |
| 2007-09-23 |
Ferruccio Guidi | fixed some file permissions (anybody can rebuild a... |
tree | commitdiff |
| 2007-09-19 |
Enrico Tassi | commented out pack coercion, since the code is not... |
tree | commitdiff |
| 2007-09-11 |
Ferruccio Guidi | librarySync - we do not generate the object attributes... |
tree | commitdiff |
| 2007-09-11 |
Enrico Tassi | replaced an assert false that cause nat_ind not to... |
tree | commitdiff |
| 2007-09-09 |
Enrico Tassi | in the case of coerce_to_sort the whd was done with... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | huge commit regarding coercions to funclass and eat_pro... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | the order of abstraction is now correct, but there... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | removed an assertion that makes no more sense to me |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | better debug printings |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | just a Pcre expression fixed, nothing real |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | matita can now safely start a matitac that will put... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | 1. fix_arity fixed: the code is totally wrong and this... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | when a coercion is passed through a case on right-param... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | ooops, missing ) |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | disabled coercions when refining paramod proofs (attemt... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | fixed propagation under Fix/Lambda/Case of coercions... |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | coercions under Fix and Case. Code refactoring needed |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | added a duplicated implementation of replace lifting |
tree | commitdiff |
| 2007-09-05 |
Ferruccio Guidi | - lybrarySync: |
tree | commitdiff |
| 2007-09-05 |
Claudio Sacerdoti... | coercions are propagated under Fix (but not mutually... |
tree | commitdiff |
| 2007-09-04 |
Claudio Sacerdoti... | Composition of coercions with arity > 0 is now implemen... |
tree | commitdiff |
| 2007-09-04 |
Claudio Sacerdoti... | 1. composition of coercions with saturations > 0 is... |
tree | commitdiff |
| 2007-08-31 |
Enrico Tassi | fixed coercions between arrows when the arrow is dependent. |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | captured exception preserved (was replaced blindly... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | reverted assertion, since it may happen to look for... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | refactoring of all coercions code and add a check to... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | bugfix in computation of src and tgt for coercions... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | Coercions rework: |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | coercions from funclass are not supported |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | added an utility function |
tree | commitdiff |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: RewriteLR were not recognized correctly... |
tree | commitdiff |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: the initial metasenv used in the two tactic... |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | Avoid reusing Hbeta several times. |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | select now works correctly even if multiple hypotheses... |
tree | commitdiff |
| 2007-08-21 |
Claudio Sacerdoti... | Avoid confusion for names of proofs put in the applicat... |
tree | commitdiff |
| 2007-08-21 |
Claudio Sacerdoti... | "obtain H E1=E2 by proof" is now working |
tree | commitdiff |
| 2007-07-31 |
Enrico Tassi | removed comments in proof presentation |
tree | commitdiff |
| 2007-07-30 |
Enrico Tassi | added 'rewrite' option to the the hint macro. a cicBrow... |
tree | commitdiff |
| 2007-07-26 |
Ferruccio Guidi | We add a binary for computing the "heights" of helm... |
tree | commitdiff |
| next |
projects / helm.git / history