| 2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
| 2009-06-18 |
denes | Added ntry and nassumption tactics |
tree | commitdiff |
| 2009-06-18 |
Claudio Sacerdoti... | 1) grafiteWalker removed |
tree | commitdiff |
| 2009-06-16 |
Claudio Sacerdoti... | 1) unification hint now takes NG terms (as it should... |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | tacticals are really tactics now, they have an AST... |
tree | commitdiff |
| 2009-06-12 |
Claudio Sacerdoti... | ocaml sucks... |
tree | commitdiff |
| 2009-06-12 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-06-12 |
Enrico Tassi | -ng implemented |
tree | commitdiff |
| 2009-06-10 |
Ferruccio Guidi | - library/list/list.ma: unused code commented |
tree | commitdiff |
| 2009-06-05 |
Ferruccio Guidi | - Procedural convertible rewrites in the conclusion... |
tree | commitdiff |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unifica... |
tree | commitdiff |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
tree | commitdiff |
| 2009-05-28 |
Ferruccio Guidi | - cicInspect: relevant nodes count updated: letin nodes... |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-18 |
Claudio Sacerdoti... | 1) GrafiteAst.NEval => GrafiteAst.NReduce |
tree | commitdiff |
| 2009-05-11 |
Claudio Sacerdoti... | - non_punctuational_tacticals ported to NG |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-05 |
Ferruccio Guidi | - Procedural: new flag "level=n" to control the reconst... |
tree | commitdiff |
| 2009-05-05 |
Ferruccio Guidi | - hExtlib: new function "list_assoc_all" |
tree | commitdiff |
| 2009-04-24 |
Claudio Sacerdoti... | Quick&dirty implementation of neqd: |
tree | commitdiff |
| 2009-04-22 |
Wilmer Ricciotti | New command "inverter" used to generate an induction... |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-14 |
Claudio Sacerdoti... | assert_tac now takes a list of sequents and also checks... |
tree | commitdiff |
| 2009-04-14 |
Claudio Sacerdoti... | New debugging tactic nassert: |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | added letin, still broken |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | new tactic whd implemented |
tree | commitdiff |
| 2009-04-08 |
Enrico Tassi | generalized is half-implemented (still broken) |
tree | commitdiff |
| 2009-04-07 |
Claudio Sacerdoti... | - nrewrite ((very?) rough implementation) |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic "case1_tac" that make "intro" followed by... |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic intro. Syntax: "# n". |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | added tentative elim |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created... |
tree | commitdiff |
| 2009-03-30 |
Enrico Tassi | tentative subst-sexpand and change |
tree | commitdiff |
| 2009-03-26 |
Enrico Tassi | new apply almost there |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-03-10 |
Enrico Tassi | unification hints almost ready |
tree | commitdiff |
| 2009-02-17 |
Ferruccio Guidi | - Coq/preamble: missing alias added |
tree | commitdiff |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | added 'unification hint command to add a term to the... |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | disambiguation can use a goal as hint for the expected... |
tree | commitdiff |
| 2008-10-17 |
Enrico Tassi | new command eval added |
tree | commitdiff |
| 2008-08-23 |
Ferruccio Guidi | Procedural: explicit flavour specification for constant... |
tree | commitdiff |
| 2008-08-21 |
Ferruccio Guidi | basic support for imposed flavour in procedural object... |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | compose tactic restore and added nocomposites keyword |
tree | commitdiff |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-07-30 |
Enrico Tassi | added 'rewrite' option to the the hint macro. a cicBrow... |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | Tentative bug fix for diverging pretty-printing function. |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | map_unicode_to_tex is no longer optional and it always... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | 1. "by proof" now allowed as a justification in equalit... |
tree | commitdiff |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose... |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented. |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
tree | commitdiff |
| 2007-05-08 |
Ferruccio Guidi | DoubleTypeInference: added a comment on "does_not_occur" |
tree | commitdiff |
| 2007-04-29 |
Ferruccio Guidi | GrafiteAstPp: \n's finally fixed |
tree | commitdiff |
| 2007-04-26 |
Ferruccio Guidi | procedural: bug fixes |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
tree | commitdiff |
| 2007-03-16 |
Ferruccio Guidi | elim tactic: it needs two arguments, a term as well... |
tree | commitdiff |
| 2007-03-13 |
Ferruccio Guidi | elim tactic: now takes a pattern instead of just a... |
tree | commitdiff |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow... |
tree | commitdiff |
| 2007-02-21 |
Ferruccio Guidi | procedural : some improvements. |
tree | commitdiff |
| 2007-02-09 |
Ferruccio Guidi | added option -dump to matitac for persistent macro... |
tree | commitdiff |
| 2007-01-24 |
Ferruccio Guidi | matitaGui: some missing cases during disambiguation... |
tree | commitdiff |
| 2007-01-10 |
Ferruccio Guidi | attributes now in the proof status: commit 4 |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | now we try two distinct depend files for compilation... |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | - tactics: |
tree | commitdiff |
| 2006-12-28 |
Claudio Sacerdoti... | .depends committed to fix non-compilation errors |
tree | commitdiff |
| 2006-12-24 |
Ferruccio Guidi | some depend files |
tree | commitdiff |
| 2006-12-20 |
Claudio Sacerdoti... | New declarative tactic "we proceed by cases on t to... |
tree | commitdiff |
| 2006-12-20 |
Claudio Sacerdoti... | New tactic cases (still to be documented). |
tree | commitdiff |
| 2006-12-19 |
Ferruccio Guidi | Procedural: "ByInduction" method ok |
tree | commitdiff |
| 2006-12-18 |
Ferruccio Guidi | Procedural: some improvements |
tree | commitdiff |
| 2006-12-14 |
Ferruccio Guidi | content2Procedural.ml: "Intros+LetTac" ok |
tree | commitdiff |
| 2006-12-12 |
Ferruccio Guidi | we started the infrastructure for the procedural render... |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | New syntax and semantics for the rewriting steps that... |
tree | commitdiff |
| 2006-11-29 |
Claudio Sacerdoti... | The rewritingstep declarative command now takes also... |
tree | commitdiff |
| 2006-11-29 |
Ferruccio Guidi | - decompose tactic: decomposable constants are now... |
tree | commitdiff |
| 2006-11-23 |
Andrea Asperti | Added a new command "index" for the indexing terms... |
tree | commitdiff |
| 2006-11-17 |
Ferruccio Guidi | helm_registry: added the pair unmarshaller |
tree | commitdiff |
| 2006-11-16 |
Ferruccio Guidi | - transcript: now outputs includes and coercions correctly |
tree | commitdiff |
| 2006-10-09 |
Claudio Sacerdoti... | applyS now receives the same parameters that auto receives. |
tree | commitdiff |
| 2006-10-03 |
maiorino | Some declarative tactics did not allow the "done" optio... |
tree | commitdiff |
| 2006-10-03 |
Claudio Sacerdoti... | Inline command implemented. |
tree | commitdiff |
| 2006-09-27 |
Claudio Sacerdoti... | Initial work on setoids: |
tree | commitdiff |
| next |
projects / helm.git / history