]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
- Procedural: generation of "exact" is now complete
[helm.git] / helm / software / components /
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete tree | commitdiff
2009-04-14 Claudio Sacerdoti... Trick: the refiner always subst-expands the outtype... tree | commitdiff
2009-04-14 Claudio Sacerdoti... Bug fixed in two lines + 5 lines of comment. 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-12 Claudio Sacerdoti... Semantic selection back again (but no semantic cut... tree | commitdiff
2009-04-12 Claudio Sacerdoti... Match is now rendered as best as possible. tree | commitdiff
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render... tree | commitdiff
2009-04-09 Claudio Sacerdoti... The substitution is now taken in account when printing... tree | commitdiff
2009-04-09 Enrico Tassiadded letin, still broken tree | commitdiff
2009-04-09 Enrico Tassinew tactic whd implemented tree | commitdiff
2009-04-09 Enrico Tassi- change implemented in 4 lines tree | commitdiff
2009-04-09 Enrico Tassi- generalize finished tree | commitdiff
2009-04-09 Enrico Tassi?_OS1 := C[ ?_IN ] tree | commitdiff
2009-04-09 Enrico Tassifixed modules order tree | commitdiff
2009-04-09 Enrico Tassiminor fixes tree | commitdiff
2009-04-09 Enrico Tassi... tree | commitdiff
2009-04-09 Claudio Sacerdoti... ... tree | commitdiff
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very... tree | commitdiff
2009-04-08 Claudio Sacerdoti... Just to make it compile again. tree | commitdiff
2009-04-08 Enrico Tassigeneralized is half-implemented (still broken) tree | commitdiff
2009-04-08 Enrico TassiAnalizyng the inductive type of the eliminated term and tree | commitdiff
2009-04-07 Claudio Sacerdoti... - nrewrite ((very?) rough implementation) tree | commitdiff
2009-04-07 Claudio Sacerdoti... - more progress towards generalize, but I am stuck now tree | commitdiff
2009-04-07 Enrico Tassi- select_tac honors the hypotheses pattern when require... tree | commitdiff
2009-04-07 Enrico Tassiselect honors the substitution tree | commitdiff
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and... tree | commitdiff
2009-04-06 Claudio Sacerdoti... ... tree | commitdiff
2009-04-06 Enrico Tassitactic cases works! delift clears tags tree | commitdiff
2009-04-06 Enrico Tassieta-contraction was made on the wrong term tree | commitdiff
2009-04-06 Enrico Tassiunification: tree | commitdiff
2009-04-06 Enrico Tassibetter error message tree | commitdiff
2009-04-06 Enrico Tassisnapshot tree | commitdiff
2009-04-05 Ferruccio Guidi- Procedural: now we generate the exact tactic (in... tree | commitdiff
2009-04-02 Enrico Tassi... tree | commitdiff
2009-04-02 Enrico TassiNew file nTacStatus to: tree | commitdiff
2009-04-02 Enrico Tassiadded analyse_indty tree | commitdiff
2009-04-01 Claudio Sacerdoti... New tactic "case1_tac" that make "intro" followed by... tree | commitdiff
2009-04-01 Claudio Sacerdoti... ## prefix is now used for tinycals tree | commitdiff
2009-04-01 Claudio Sacerdoti... New tactic intro. Syntax: "# n". tree | commitdiff
2009-04-01 Enrico Tassiadded tentative elim tree | commitdiff
2009-04-01 Enrico Tassi1) mk_meta now returns also the index of the created... tree | commitdiff
2009-04-01 Enrico Tassiremoved spurious " tree | commitdiff
2009-03-30 Enrico Tassitentative subst-sexpand and change tree | commitdiff
2009-03-30 Enrico Tassi... tree | commitdiff
2009-03-27 Enrico Tassimore comments tree | commitdiff
2009-03-27 Enrico Tassiexec and distribute implemented tree | commitdiff
2009-03-26 Enrico Tassinew apply almost there tree | commitdiff
2009-03-25 Enrico Tassinew tactics are almost ready tree | commitdiff
2009-03-16 Andrea AspertiNew parameters for applyS: 10 20. tree | commitdiff
2009-03-11 Ferruccio GuidiProcedural: id tactics are not counted, ie they are... tree | commitdiff
2009-03-11 Ferruccio Guidibug fix + better obj flavour guessing via inner sorts tree | commitdiff
2009-03-11 Ferruccio Guidithe level 1 reconstruction procedure is now in Procedural1 tree | commitdiff
2009-03-11 Ferruccio Guidi.... tree | commitdiff
2009-03-11 Ferruccio Guidinew dependences tree | commitdiff
2009-03-11 Enrico Tassiunification hints with recursive calls do work! tree | commitdiff
2009-03-11 Enrico Tassiadded margin option to the pp tree | commitdiff
2009-03-10 Enrico Tassiunificatiom hints with premises tree | commitdiff
2009-03-10 Enrico Tassiunification hints almost ready tree | commitdiff
2009-03-10 Andrea AspertiA version of applyS with bounded iterations of given_cl... tree | commitdiff
2009-03-10 Andrea AspertiRemoved the context from the metasenv to avoid trivial... tree | commitdiff
2009-03-03 Enrico Tassi- fixed hint generation, more hints are generated tree | commitdiff
2009-03-02 Ferruccio GuidicicInspect: node count fixed tree | commitdiff
2009-02-26 Ferruccio GuidicicInspect: now we can choose not to count the Cic... tree | commitdiff
2009-02-25 Ferruccio GuidiProceduralTeX completed and tested on the terms given... tree | commitdiff
2009-02-21 Ferruccio GuidiNew module for TeX rendering of procedural input/output tree | commitdiff
2009-02-20 Enrico Tassi... tree | commitdiff
2009-02-17 Ferruccio Guidi- Coq/preamble: missing alias added tree | commitdiff
2009-02-15 Enrico Tassicommented some printings tree | commitdiff
2009-02-12 Andrea Aspertierrata corrige. tree | commitdiff
2009-02-12 Andrea AspertiFixed a problem of lifting. tree | commitdiff
2009-02-11 Enrico Tassisome work to refine objs tree | commitdiff
2009-02-05 Enrico Tassia non necessary but morally required change. The matche... tree | commitdiff
2009-02-03 Enrico Tassicase tactic first tries with a simple outtype and then... tree | commitdiff
2009-02-02 Enrico TassiCicTypeChecker.typecheck now takes an additional parameter: tree | commitdiff
2009-01-30 Enrico Tassifix convertibility in case of application test_eq_only... tree | commitdiff
2009-01-29 Enrico Tassiapplication arguments are compared with test_eq_only... tree | commitdiff
2009-01-26 Enrico Tassimaction layout added to notation tree | commitdiff
2009-01-26 Enrico Tassiwe were generating a name for the main fix twice tree | commitdiff
2009-01-26 Enrico Tassiadded a number to identical error messages to ease... tree | commitdiff
2009-01-19 Enrico Tassiall pullbacks are attempted in sequence, removed many... tree | commitdiff
2009-01-16 Enrico Tassiceommented out metasenv tree | commitdiff
2009-01-15 Enrico Tassiif the user attempts to insert a duplicate coercions... tree | commitdiff
2009-01-15 Enrico Tassiunvariant also for coercions to funclass tree | commitdiff
2009-01-15 Enrico Tassi- name mangling changed, added __ to separate additiona... tree | commitdiff
2009-01-15 Enrico Tassino more universe inconsistency printed to stderr tree | commitdiff
2009-01-15 Enrico Tassicoercions that are marked as variant are unfolded when... tree | commitdiff
2009-01-15 Enrico TassiCoercions graph is printed between real types and not... tree | commitdiff
2009-01-13 Enrico Tassimany changes regarding coercions: tree | commitdiff
2009-01-08 Enrico Tassimore composites to make all happy! tree | commitdiff
2009-01-06 Enrico Tassicoercions reordering implemented tree | commitdiff
2009-01-05 Enrico Tassiremoving (only from the interface) functions related... tree | commitdiff
2008-12-24 Enrico Tassibug fixed, all convertible was called without a metasenv tree | commitdiff
2008-12-19 Enrico Tassimore pps tree | commitdiff
2008-12-19 Enrico Tassitype3 tree | commitdiff
2008-12-19 Enrico Tassiranking hopefully fixed tree | commitdiff
2008-12-19 Enrico Tassibetter pps tree | commitdiff
2008-12-19 Enrico Tassihandles bad Appl tree | commitdiff
2008-12-19 Enrico Tassiadded better debug_pps and add_user_provided_unificatio... tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.