2006-07-13 |
Stefano Zacchiroli | use the graphviz pretty printer to generate graphviz... |
tree | commitdiff |
2006-07-13 |
Stefano Zacchiroli | moved graphviz pretty printer outside matita, so that... |
tree | commitdiff |
2006-07-12 |
Stefano Zacchiroli | generate dot files with attributes on nodes (instead... |
tree | commitdiff |
2006-07-12 |
Stefano Zacchiroli | added uri_of_carr |
tree | commitdiff |
2006-07-12 |
Claudio Sacerdoti... | Missing copyright added to tactics/declarative.ml* |
tree | commitdiff |
2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Quit (unused) removed. |
tree | commitdiff |
2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Print (unused) removed. |
tree | commitdiff |
2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Search_pat and GrafiteAst.Search_term (both... |
tree | commitdiff |
2006-07-11 |
maiorino | First experimental version of the declarative proof... |
tree | commitdiff |
2006-07-11 |
Enrico Tassi | - removed Positive and Negative (all is positive) |
tree | commitdiff |
2006-07-10 |
Enrico Tassi | ... |
tree | commitdiff |
2006-07-10 |
Enrico Tassi | improved coercions support: |
tree | commitdiff |
2006-07-10 |
Enrico Tassi | fixed 1,2: and *: according to the camera ready semantics |
tree | commitdiff |
2006-07-10 |
Enrico Tassi | added flatten_map |
tree | commitdiff |
2006-07-06 |
Enrico Tassi | fixed *: and n,m: |
tree | commitdiff |
2006-07-05 |
Enrico Tassi | bugfix to developments: |
tree | commitdiff |
2006-07-03 |
Enrico Tassi | - patch to consider the symbols of the goal when comput... |
tree | commitdiff |
2006-06-30 |
Enrico Tassi | pretty proofs are back |
tree | commitdiff |
2006-06-29 |
Andrea Asperti | Cleaning up; removed a couple of "open". |
tree | commitdiff |
2006-06-29 |
Claudio Sacerdoti... | Demodulate used to be a reduction_kind and it used... |
tree | commitdiff |
2006-06-29 |
Claudio Sacerdoti... | WORK IN PROGRESS: |
tree | commitdiff |
2006-06-29 |
Enrico Tassi | before goals are inferred with current, |
tree | commitdiff |
2006-06-29 |
Enrico Tassi | goals after a superposition step are relocated |
tree | commitdiff |
2006-06-28 |
Ferruccio Guidi | - "linear" flag added to lapply (automatic clearing) |
tree | commitdiff |
2006-06-28 |
Enrico Tassi | karma: every term the rewrite acts on must be substututed |
tree | commitdiff |
2006-06-28 |
Enrico Tassi | superposition_left not performed if the input goal... |
tree | commitdiff |
2006-06-27 |
Ferruccio Guidi | - decompose now runs with no arguments (operates on... |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | fixed infer_goal, added simplification before inferring... |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | using the new metadataConstraint function |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | used the new metadataConstraint function to retrieve... |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | fixed equalities_for_goal |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | the old compute_eq_weight is back (no more max) |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | fixed generation of letins |
tree | commitdiff |
2006-06-27 |
Enrico Tassi | added a metas_of_term implemented using sets instead... |
tree | commitdiff |
2006-06-26 |
Enrico Tassi | more work for the generic auto parameters |
tree | commitdiff |
2006-06-21 |
Enrico Tassi | added the geniric |
tree | commitdiff |
2006-06-20 |
Ferruccio Guidi | - fwd concrete syntax fixed |
tree | commitdiff |
2006-06-20 |
Enrico Tassi | garbage collection of dead equalities implemented |
tree | commitdiff |
2006-06-20 |
Ferruccio Guidi | - added some documentation on the fwd tatcic |
tree | commitdiff |
2006-06-19 |
Enrico Tassi | typo cpying the formal semantic |
tree | commitdiff |
2006-06-19 |
Enrico Tassi | reorganized guiven_clause to work with the on_the_fly... |
tree | commitdiff |
2006-06-19 |
Enrico Tassi | demodulation of goal activated again. |
tree | commitdiff |
2006-06-19 |
Andrea Asperti | some experiments |
tree | commitdiff |
2006-06-19 |
Andrea Asperti | added (but still unused) remove_local_context |
tree | commitdiff |
2006-06-19 |
Andrea Asperti | added (but not yet used) remove_local_context |
tree | commitdiff |
2006-06-19 |
Andrea Asperti | Utils.compare_terms instead of compare_weights |
tree | commitdiff |
2006-06-19 |
Andrea Asperti | occur_check and unification fixed. now Meta(i,[]) and... |
tree | commitdiff |
2006-06-18 |
Enrico Tassi | - some fixes regarding URIs of equality that now should... |
tree | commitdiff |
2006-06-18 |
Enrico Tassi | instead of including library_notation we include logic... |
tree | commitdiff |
2006-06-16 |
Enrico Tassi | ancient bug solved. if the term is (eq TY A B) the... |
tree | commitdiff |
2006-06-16 |
Enrico Tassi | some more on equalities |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added! |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | added applyS |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | some fixed done in Orsay: |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | exported 2 functions needed by applyS |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | ... |
tree | commitdiff |
2006-06-15 |
Andrea Asperti | default constants are now the matita standard library... |
tree | commitdiff |
2006-06-14 |
Stefano Zacchiroli | removed old debugging print |
tree | commitdiff |
2006-06-13 |
Stefano Zacchiroli | moved benchmnarks/ dir outside of components/ |
tree | commitdiff |
2006-06-11 |
Ferruccio Guidi | - slight fix in lapply syntax |
tree | commitdiff |
2006-06-09 |
Claudio Sacerdoti... | Syntactic bug changed: t in "unfold t" must be a tactic... |
tree | commitdiff |
2006-06-09 |
Claudio Sacerdoti... | 1. the default for the default equality/absurd/true... |
tree | commitdiff |
2006-06-01 |
Stefano Zacchiroli | implemented tinycals: |
tree | commitdiff |
2006-06-01 |
Stefano Zacchiroli | commented the finally function |
tree | commitdiff |
2006-06-01 |
Enrico Tassi | fix |
tree | commitdiff |
2006-06-01 |
Enrico Tassi | ... |
tree | commitdiff |
2006-06-01 |
Enrico Tassi | ... |
tree | commitdiff |
2006-06-01 |
Stefano Zacchiroli | use the appropriate chain of transormations for pretty... |
tree | commitdiff |
2006-06-01 |
Stefano Zacchiroli | made pp_term parametric and explained the proper way... |
tree | commitdiff |
2006-06-01 |
Andrea Asperti | Subsumption_subst must be applied to the initial proof... |
tree | commitdiff |
2006-05-31 |
Enrico Tassi | \n restored |
tree | commitdiff |
2006-05-31 |
Enrico Tassi | fixed proofs, contextualization should now work. |
tree | commitdiff |
2006-05-30 |
Claudio Sacerdoti... | Bug fixed: theories were handled as base uris, not... |
tree | commitdiff |
2006-05-30 |
Enrico Tassi | letin are now sorted properly. |
tree | commitdiff |
2006-05-30 |
Enrico Tassi | fixed proof generation again |
tree | commitdiff |
2006-05-30 |
Claudio Sacerdoti... | ZACK: export a top level function for parsing terms... |
tree | commitdiff |
2006-05-30 |
Enrico Tassi | A -> Univ |
tree | commitdiff |
2006-05-30 |
Enrico Tassi | canonical and contextualize_rewrites are back, they... |
tree | commitdiff |
2006-05-30 |
Enrico Tassi | the function to create on the fly a symmetry step has... |
tree | commitdiff |
2006-05-29 |
Enrico Tassi | profilings are printed |
tree | commitdiff |
2006-05-29 |
Enrico Tassi | - proofs by subsumption now add a symmetry step if... |
tree | commitdiff |
2006-05-29 |
Claudio Sacerdoti... | bug fix: use an (un)marshaller for get_opt instead... |
tree | commitdiff |
2006-05-29 |
Claudio Sacerdoti... | Bug fixed in fresh_name_generator: the function used... |
tree | commitdiff |
2006-05-28 |
Enrico Tassi | weak equality on meta used when replacing. |
tree | commitdiff |
2006-05-28 |
Enrico Tassi | added the rule field to goal_proof. |
tree | commitdiff |
2006-05-28 |
Enrico Tassi | - fixed a bug in unification (not sure in the right... |
tree | commitdiff |
2006-05-26 |
Claudio Sacerdoti... | Recently introduced bug in CicRefine.eat_prods fixed... |
tree | commitdiff |
2006-05-26 |
Claudio Sacerdoti... | Great optimization for eat_prods: if the type of the... |
tree | commitdiff |
2006-05-26 |
Andrea Asperti | 1) variables occurring only in proofs anre not relocated |
tree | commitdiff |
2006-05-26 |
Claudio Sacerdoti... | Profiling code removed. |
tree | commitdiff |
2006-05-26 |
Andrea Asperti | Bug fixed: the syntax "?n" used to be broken. It tried... |
tree | commitdiff |
2006-05-25 |
Claudio Sacerdoti... | Added debug menu item to restrict disambiguation to... |
tree | commitdiff |
2006-05-25 |
Claudio Sacerdoti... | Axioms are not allowed with the syntax: "axiom name... |
tree | commitdiff |
2006-05-23 |
Andrea Asperti | added important comment |
tree | commitdiff |
2006-05-23 |
Andrea Asperti | fixed LetIn proofs |
tree | commitdiff |
2006-05-23 |
Enrico Tassi | added again stuff for profiling |
tree | commitdiff |
2006-05-23 |
Enrico Tassi | added dependency on Str |
tree | commitdiff |
2006-05-23 |
Enrico Tassi | ... |
tree | commitdiff |
2006-05-23 |
Andrea Asperti | added stuff for profiling macros |
tree | commitdiff |
2006-05-22 |
Enrico Tassi | - code cleanup, especialli in Indexing where all the... |
tree | commitdiff |
next |