]> matita.cs.unibo.it Git - helm.git/history - helm/software
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
add comment
[helm.git] / helm / software /
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (part B, by CSC :-): tree | commitdiff
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (by CSC,actuall :-) tree | commitdiff
2009-06-15 Enrico Tassi... tree | commitdiff
2009-06-15 Enrico Tassiadded TODO list tree | commitdiff
2009-06-15 Enrico Tassihuge commit regarding the grafite_status: tree | commitdiff
2009-06-15 Enrico Tassipart of last commit tree | commitdiff
2009-06-15 Enrico Tassitacticals are really tactics now, they have an AST... tree | commitdiff
2009-06-13 Ferruccio Guidiwe removed some coercion detours and we added some... tree | commitdiff
2009-06-12 denesImplemented keep_simplified. 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-12 Andrea AspertiAdded a new keep_simplified function tree | commitdiff
2009-06-12 Andrea AspertiRenamed forward_simplify into simplify and backward_sim... tree | commitdiff
2009-06-11 denesActive goals are now demodulated after selecting a... tree | commitdiff
2009-06-11 Ferruccio Guidi- applyTransformation: bugfix in the rendering of records tree | commitdiff
2009-06-11 Enrico Tassicontent2pres for the new cic fixed tree | commitdiff
2009-06-11 Ferruccio Guidi- some depend files fixed tree | commitdiff
2009-06-10 Ferruccio Guidi- library/list/list.ma: unused code commented tree | commitdiff
2009-06-10 Enrico Tassi1) added simplification of actives w.r.t. selected tree | commitdiff
2009-06-10 Enrico Tassiright inference step completed tree | commitdiff
2009-06-10 Enrico Tassinew function filter_map_acc tree | commitdiff
2009-06-10 denesExtended the equality case to non ground terms tree | commitdiff
2009-06-09 Ferruccio Guidi- Procedural: more support for the Debug inline option... tree | commitdiff
2009-06-09 Claudio Sacerdoti... Debugging code removed. tree | commitdiff
2009-06-09 Claudio Sacerdoti... Temporary (and partially broken) patch for Ferruccio... tree | commitdiff
2009-06-09 Enrico Tassialmost complete superposition right step tree | commitdiff
2009-06-09 Enrico Tassisnapshot tree | commitdiff
2009-06-09 Enrico Tassisee the previous commit tree | commitdiff
2009-06-09 Enrico TassitermAcicContent is logic independent (despite its name... tree | commitdiff
2009-06-09 denesOptimized weigths comparison, removed normalization tree | commitdiff
2009-06-09 Enrico Tassisnaphost: supright almost done tree | commitdiff
2009-06-09 Enrico Tassi... tree | commitdiff
2009-06-09 Enrico Tassi... tree | commitdiff
2009-06-09 denesImplemented substitution application and concatenation tree | commitdiff
2009-06-09 Enrico Tassi... tree | commitdiff
2009-06-09 Enrico Tassifixed metas tree | commitdiff
2009-06-09 Enrico Tassifixed building tree | commitdiff
2009-06-08 Enrico Tassi... tree | commitdiff
2009-06-08 Enrico Tassia skeleton of supright tree | commitdiff
2009-06-08 Enrico Tassisome more functors and a nice higher-order all_position... tree | commitdiff
2009-06-08 Enrico Tassiadded META for ng_paramodulation tree | commitdiff
2009-06-06 Claudio Sacerdoti... Previous commit reverted, as explained in that log. tree | commitdiff
2009-06-06 Claudio Sacerdoti... This commit restores the ids_to_father_ids table. tree | commitdiff
2009-06-06 Enrico Tassisome renaming to make ocamlopt happy tree | commitdiff
2009-06-05 Ferruccio Guidibugfix in Include syntax: it was changed and committed... tree | commitdiff
2009-06-05 Ferruccio Guidi- Procedural convertible rewrites in the conclusion... tree | commitdiff
2009-06-05 denesFirst tests for paramodulation (pretty printer, unifica... tree | commitdiff
2009-06-05 Wilmer Ricciotti- replaced part1a/defn with the version based on induct... tree | commitdiff
2009-06-05 denesFix : wrong exception was catch in apply_subst tree | commitdiff
2009-06-05 Claudio Sacerdoti... 1) the home button of CicBrowser now works also for NG tree | commitdiff
2009-06-05 Claudio Sacerdoti... The kernel _must_ check the correctness of the height... tree | commitdiff
2009-06-04 Ferruccio Guidisyntax error fixed :( tree | commitdiff
2009-06-04 Ferruccio Guidi- doubleTypeInference: we check for unreferenced letins... tree | commitdiff
2009-06-04 denesFirst pretty printing functions tree | commitdiff
2009-06-04 Enrico Tassiminor changes here and there. We extend fo-unification... tree | commitdiff
2009-06-04 Enrico Tassicomments tree | commitdiff
2009-06-04 Enrico Tassibetter type for comparison and implementation of KBO... tree | commitdiff
2009-06-04 Enrico Tassimore functors tree | commitdiff
2009-06-03 Ferruccio Guidi- boxPp: added missing spaces tree | commitdiff
2009-06-03 Wilmer RicciottiUpdate, using induction/inversion. tree | commitdiff
2009-06-03 Enrico Tassifunctorial abstraction over term blobs tree | commitdiff
2009-06-03 Andrea Aspertinot_to_not tree | commitdiff
2009-06-03 Claudio Sacerdoti... New test for NG notation. tree | commitdiff
2009-06-03 Claudio Sacerdoti... Huge commit with several changes: tree | commitdiff
2009-06-01 denesFirst implementation of unification on foterms tree | commitdiff
2009-06-01 denesFirst functions on substitutions for unification tree | commitdiff
2009-06-01 Enrico Tassiadded a snapshot of comparison tree | commitdiff
2009-06-01 Andrea AspertiThis works for me tree | commitdiff
2009-06-01 Enrico Tassiwe rewrite the paramodulation code! tree | commitdiff
2009-05-29 Wilmer RicciottiPOPLmark part 1a using the de Bruijn encoding. tree | commitdiff
2009-05-29 Ferruccio Guidi- cicNotationParser: added extra space to TeX control... tree | commitdiff
2009-05-28 Ferruccio GuidiProcedural: higher-order unification needs a lot of... tree | commitdiff
2009-05-28 Ferruccio Guidi- cicInspect: relevant nodes count updated: letin nodes... tree | commitdiff
2009-05-27 Ferruccio GuidiProcedural: bugfix in the generation of intros for... tree | commitdiff
2009-05-27 Ferruccio Guidi- Procedural: we specify more unifiers for apply to... tree | commitdiff
2009-05-27 Claudio Sacerdoti... Basic support for interpretations for NG: tree | commitdiff
2009-05-27 Andrea AspertiAvoiding to filter the application of congruence equations tree | commitdiff
2009-05-26 Claudio Sacerdoti... ... tree | commitdiff
2009-05-26 Claudio Sacerdoti... ... tree | commitdiff
2009-05-26 Andrea Aspertiremoved a call to autobatch. tree | commitdiff
2009-05-25 Enrico Tassinasty change in the lexer/parser: tree | commitdiff
2009-05-22 Ferruccio Guidibugfix in the output notation for eq tree | commitdiff
2009-05-22 Andrea AspertiPruning candidates in the applicative case for equalities. tree | commitdiff
2009-05-21 Ferruccio GuidiProcedural: we use the expected type rather than the... tree | commitdiff
2009-05-21 Ferruccio Guidi- cicUtil: is_sober now detects non-positive rels. tree | commitdiff
2009-05-21 Andrea Aspertiautobatch -> autobatch by tree | commitdiff
2009-05-20 Ferruccio Guidiwe catch the refiner errors in the critical step and... tree | commitdiff
2009-05-20 Andrea AspertiRemoved a silly type check tree | commitdiff
2009-05-19 Enrico Tassi... tree | commitdiff
2009-05-19 Andrea AspertiNotEq is now considered as a negative Eq atom tree | commitdiff
2009-05-19 Enrico Tassiregenerated tree | commitdiff
2009-05-19 Enrico Tassifixed generation of horn clauses, negated atoms are... tree | commitdiff
2009-05-19 Enrico Tassisome horn+equality problems tree | commitdiff
2009-05-18 Claudio Sacerdoti... removed byte queries tree | commitdiff
2009-05-18 Enrico Tassiremoved useless function tree | commitdiff
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i... tree | commitdiff
2009-05-18 Enrico Tassinothing special tree | commitdiff
2009-05-18 Claudio Sacerdoti... 1) GrafiteAst.NEval => GrafiteAst.NReduce tree | commitdiff
2009-05-18 Claudio Sacerdoti... 1) new tactic normalize (low-level function implemented in tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.