]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
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...
2009-05-15 Claudio Sacerdoti... Cosmetic.
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
2009-05-14 Ferruccio Guidi- libraryObjects: new default "natural numbers" with...
2009-05-13 Ferruccio Guidiinterpretations placed right after the corresponding...
2009-05-13 Ferruccio Guidi- matitaEngine: some commands like "coercion" must...
2009-05-13 Andrea AspertiThe singature of the "by" universe is added to the...
2009-05-13 Andrea AspertiVia un'altra linea...
2009-05-13 Andrea AspertiSempre piu' breve
2009-05-13 Andrea AspertiSignature is computed on the initial goal, once and...
2009-05-12 Claudio Sacerdoti... Do we really want to generate eliminators for nested...
2009-05-12 Claudio Sacerdoti... All weakly positive types but imbricated ones are now...
2009-05-12 Ferruccio Guidi- Procedural: we now reconstruct "let H := v in t"...
2009-05-12 Andrea AspertiWe only filter the smart candidates w.r.t the signature
2009-05-11 Claudio Sacerdoti... Some experiments in generation of elimination principles.
2009-05-11 Claudio Sacerdoti... ppsubst commented out in ppobj
2009-05-11 Claudio Sacerdoti... Bug fixed: the relevance list can be shorted then leftn...
2009-05-11 Claudio Sacerdoti... Missing spaces inserted here and there.
2009-05-11 Claudio Sacerdoti... - non_punctuational_tacticals ported to NG
2009-05-11 Claudio Sacerdoti... Buffers are now used everywhere for speed-up.
2009-05-11 Claudio Sacerdoti... New function list_iter_sep.
2009-05-11 Andrea AspertiA few lemmas about inclusion.
2009-05-11 Andrea AspertiMore automation
2009-05-10 Claudio Sacerdoti... - critical bug fixed in NCicSubstitution.lift:
2009-05-08 Claudio Sacerdoti... Stupid typing error fixed.
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Claudio Sacerdoti... Bug fixed: left parameters of constructors were unified...
2009-05-08 Claudio Sacerdoti... Bug fixed: refinement of mutual recursive definitions...
2009-05-08 Claudio Sacerdoti... Improved tests (for left parameters and mutual recursiv...
2009-05-08 Claudio Sacerdoti... Bug fixed in refinement of inductive types: left parame...
2009-05-08 Claudio Sacerdoti... 1) better implementation of NObj that now calls recursi...
2009-05-08 Claudio Sacerdoti... The relevance list can be shorter than leftno (when...
2009-05-08 Claudio Sacerdoti... Bug fixed in interpretation of records (the type was...
2009-05-08 Andrea AspertiConstructors are closed with thier types when computing...
2009-05-08 Andrea Aspertiversione automatizzata
2009-05-08 Andrea Aspertisymmetry of inequality sym_neq
2009-05-07 Ferruccio Guididocumentation for the inline command
2009-05-06 Ferruccio Guidi- dependenciesParser: updated to new inline syntax
2009-05-06 Ferruccio GuidiLAMBDA-TYPES: mma's recommitted because inline syntax...
2009-05-06 Ferruccio Guidi- cicUtil: is_sober now detects folded applications
2009-05-06 Enrico Tassiapply and auto.equational_case call saturation.solve_na...
2009-05-06 Enrico Tassiupdated comment
2009-05-05 Ferruccio Guidi- Procedural: new flag "level=n" to control the reconst...
2009-05-05 Ferruccio Guidi- hExtlib: new function "list_assoc_all"
2009-05-05 Enrico Tassi- pretty printer made robust in face of list_nth
2009-05-05 Enrico Tassimore tests
2009-05-05 Andrea AspertiNuova gestione di "by" per auto.
2009-05-05 Andrea Aspertiautobatch by
next