| 2009-04-29 |
Enrico Tassi | many checks guarded with if Utils.debug_metas
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | depenalization of smart apply inside auto, that is...
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | fixed bug, demodulation was keeping results not strictly...
|
commit | commitdiff | tree |
| 2009-04-28 |
Enrico Tassi | huge commit in automation:
|
commit | commitdiff | tree |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present...
|
commit | commitdiff | tree |
| 2009-04-21 |
Enrico Tassi | fixed last file restricting auto tables
|
commit | commitdiff | tree |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_cache
|
commit | commitdiff | tree |
| 2009-04-16 |
Enrico Tassi | Universe is used only locally to tactics/
|
commit | commitdiff | tree |
| 2009-04-16 |
Enrico Tassi | added an exception
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | added letin, still broken
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | new tactic whd implemented
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | - change implemented in 4 lines
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | - generalize finished
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ?_OS1 := C[ ?_IN ]
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | fixed modules order
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | minor fixes
|
commit | commitdiff | tree |
| 2009-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-08 |
Enrico Tassi | generalized is half-implemented (still broken)
|
commit | commitdiff | tree |
| 2009-04-08 |
Enrico Tassi | Analizyng the inductive type of the eliminated term and
|
commit | commitdiff | tree |
| 2009-04-07 |
Enrico Tassi | - select_tac honors the hypotheses pattern when required...
|
commit | commitdiff | tree |
| 2009-04-07 |
Enrico Tassi | select honors the substitution
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | eta-contraction was made on the wrong term
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | unification:
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | better error message
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | added one exception
|
commit | commitdiff | tree |
| 2009-04-06 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2009-04-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-04-02 |
Enrico Tassi | New file nTacStatus to:
|
commit | commitdiff | tree |
| 2009-04-02 |
Enrico Tassi | added analyse_indty
|
commit | commitdiff | tree |
| 2009-04-01 |
Enrico Tassi | added tentative elim
|
commit | commitdiff | tree |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created...
|
commit | commitdiff | tree |
| 2009-04-01 |
Enrico Tassi | removed spurious "
|
commit | commitdiff | tree |
| 2009-03-30 |
Enrico Tassi | tentative subst-sexpand and change
|
commit | commitdiff | tree |
| 2009-03-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-03-27 |
Enrico Tassi | more comments
|
commit | commitdiff | tree |
| 2009-03-27 |
Enrico Tassi | exec and distribute implemented
|
commit | commitdiff | tree |
| 2009-03-26 |
Enrico Tassi | new apply almost there
|
commit | commitdiff | tree |
| 2009-03-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-03-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready
|
commit | commitdiff | tree |
| 2009-03-16 |
Enrico Tassi | added mactions, the three can now be collapsed to fit...
|
commit | commitdiff | tree |
| 2009-03-11 |
Enrico Tassi | unification hints with recursive calls do work!
|
commit | commitdiff | tree |
| 2009-03-11 |
Enrico Tassi | added margin option to the pp
|
commit | commitdiff | tree |
| 2009-03-11 |
Enrico Tassi | more examples
|
commit | commitdiff | tree |
| 2009-03-10 |
Enrico Tassi | unificatiom hints with premises
|
commit | commitdiff | tree |
| 2009-03-10 |
Enrico Tassi | unification hints almost ready
|
commit | commitdiff | tree |
| 2009-03-10 |
Enrico Tassi | notation ++
|
commit | commitdiff | tree |
| 2009-03-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated
|
commit | commitdiff | tree |
| 2009-02-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-20 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-16 |
Enrico Tassi | some notational experiments
|
commit | commitdiff | tree |
| 2009-02-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-15 |
Enrico Tassi | commented some printings
|
commit | commitdiff | tree |
| 2009-02-15 |
Enrico Tassi | minor changes to make the library compile after wilmers...
|
commit | commitdiff | tree |
| 2009-02-11 |
Enrico Tassi | some work to refine objs
|
commit | commitdiff | tree |
| 2009-02-11 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-09 |
Enrico Tassi | b:action are now considered as m:maction and thus are...
|
commit | commitdiff | tree |
| 2009-02-06 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-05 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-05 |
Enrico Tassi | a non necessary but morally required change. The matched...
|
commit | commitdiff | tree |
| 2009-02-03 |
Enrico Tassi | some work to speed up the system
|
commit | commitdiff | tree |
| 2009-02-03 |
Enrico Tassi | case tactic first tries with a simple outtype and then...
|
commit | commitdiff | tree |
| 2009-02-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-02-02 |
Enrico Tassi | CicTypeChecker.typecheck now takes an additional parameter:
|
commit | commitdiff | tree |
| 2009-01-30 |
Enrico Tassi | fix convertibility in case of application test_eq_only...
|
commit | commitdiff | tree |
| 2009-01-29 |
Enrico Tassi | more polishing
|
commit | commitdiff | tree |
| 2009-01-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-29 |
Enrico Tassi | application arguments are compared with test_eq_only...
|
commit | commitdiff | tree |
| 2009-01-28 |
Enrico Tassi | some work
|
commit | commitdiff | tree |
| 2009-01-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-27 |
Enrico Tassi | maction, mpadded and mstyle added to documentation
|
commit | commitdiff | tree |
| 2009-01-26 |
Enrico Tassi | minor fixes
|
commit | commitdiff | tree |
| 2009-01-26 |
Enrico Tassi | maction support added to notation, adopted for = AKA...
|
commit | commitdiff | tree |
| 2009-01-26 |
Enrico Tassi | maction layout added to notation
|
commit | commitdiff | tree |
| 2009-01-26 |
Enrico Tassi | we were generating a name for the main fix twice
|
commit | commitdiff | tree |
| 2009-01-26 |
Enrico Tassi | added a number to identical error messages to ease...
|
commit | commitdiff | tree |
| 2009-01-21 |
Enrico Tassi | some minor fixes
|
commit | commitdiff | tree |
| 2009-01-21 |
Enrico Tassi | a bit of work done while travelling to padova
|
commit | commitdiff | tree |
| 2009-01-19 |
Enrico Tassi | - new notation.ma file with local and common notation
|
commit | commitdiff | tree |
| 2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many...
|
commit | commitdiff | tree |
| 2009-01-16 |
Enrico Tassi | ceommented out metasenv
|
commit | commitdiff | tree |
| 2009-01-16 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | the new coercion behaviour (variants + composition...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | added notation for 'Vdash
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | if the user attempts to insert a duplicate coercions...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | unvariant also for coercions to funclass
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | - name mangling changed, added __ to separate additional...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | no more universe inconsistency printed to stderr
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | coercions that are marked as variant are unfolded when...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search