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