]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
- lambda_notation.ma: more notation and bug fixes
[helm.git] / helm / software / components /
2010-03-04 Andrea AspertiCorrected a bug relative to the application of substs...
2010-03-02 Wilmer RicciottiAdded syntax for ninversion tactic (still experimental).
2010-03-02 Enrico TassiConstants are indexed using the Reference, not the...
2010-03-01 Wilmer RicciottiFixed a bug in the unification, which prevented some...
2010-02-19 Andrea AspertiOpen goals fixed (it also returned closed goals).
2010-02-19 Andrea AspertiRemoved debug printings.
2010-02-19 Andrea Aspertiadded lazy
2010-02-19 Andrea AspertiNuova versione di auto.
2010-02-19 Andrea AspertiAdded an implicit parameter to branch_tac to allow...
2010-02-15 Claudio Sacerdoti... The height of fixpoint applications was not computed...
2010-02-11 Enrico Tassiminimal sequent height set to 1
2010-02-11 Enrico Tassisome experiment filtering with height
2010-02-09 Andrea AspertiAdded a count_occurrences function.
2010-02-08 Andrea AspertiBug fixing.
2010-02-08 Andrea AspertiRemoved debug printings.
2010-02-08 Andrea AspertiSome changes towards integration of setoid-rewriting.
2010-02-04 Andrea AspertiAdded count_occurrences.
2010-02-03 Claudio Sacerdoti... ...
2010-02-03 Wilmer RicciottiDisabled debug prints in ndestruct tactic.
2010-02-03 Claudio Sacerdoti... Debug code commented out.
2010-02-03 Claudio Sacerdoti... Parts of the status were not re-initialized correctly...
2010-02-03 Claudio Sacerdoti... Bad variable name fixed.
2010-02-03 Claudio Sacerdoti... Bug fixed: projection redexes obtained reducing other...
2010-02-02 Wilmer RicciottiNew version using Streicher's K axiom. Should be faster...
2010-02-02 Wilmer RicciottiFixed a bug with indexed inductive types which sometime...
2010-02-01 Andrea AspertiOn the last goal at maxdepth we stop at the first solution.
2010-01-29 Andrea AspertiNuova gestione della width.
2010-01-27 Andrea AspertiUnfolded exact letins during proof reconstruction.
2010-01-27 Andrea AspertiAdded a parameter no_implicit (default true) to choose...
2010-01-18 Andrea AspertiNew paramod tac.
2010-01-18 Andrea AspertiInvocation of paramod
2010-01-18 Andrea Aspertiparamod_tac exported
2010-01-18 Andrea AspertiNumber notation for NG
2010-01-18 Andrea AspertiNumber notation for NG
2010-01-18 Andrea AspertiNumber notation for NG.
2010-01-18 Andrea AspertiKeeping Implicit for refinement (instead of transformin...
2010-01-12 Wilmer RicciottiFixed a bug in the discrimination principle: the refine...
2010-01-11 Andrea Asperti1. New paramodulation function
2010-01-11 Andrea Aspertisaturate cust be called with delta=0
2010-01-11 Andrea AspertiAdded is_equation
2010-01-11 Andrea AspertiDebugging info
2010-01-08 Andrea AspertiThe body of constants is a reference, not the actual...
2010-01-08 Andrea Aspertiremoved debugging info
2010-01-08 Andrea AspertiapplyS
2010-01-08 Andrea Aspertirefresh uri
2010-01-08 Andrea AspertiSupport for the new auto tactics //
2010-01-08 Andrea AspertiSupport for the new // tactics.
2010-01-08 Andrea Aspertinew reloc_subst (to avoid cyclic substitutions).
2009-12-21 Andrea AspertiRefining with no expected type + unification seems...
2009-12-21 Andrea AspertiTrying to be faster
2009-12-21 Andrea AspertiTrying to be faster.
2009-12-18 Andrea AspertiFinal subst returned by superposition and passed around.
2009-12-18 Andrea Aspertiusing = instead of alpha conversions. context metasenv...
2009-12-10 Andrea AspertiMinor bag fixed, relative to failures.
2009-12-10 Andrea AspertiA compiling version?
2009-12-09 Andrea AspertiAdded a "sort_metasenv" function.
2009-12-09 Andrea AspertiCommented a couple of calls to "set_reference_of_oxuri".
2009-12-09 Andrea AspertiAdded the paramodulation stuff to the status
2009-12-09 Andrea Aspertiparam "slir" to call the new auto
2009-12-09 Andrea AspertiAdded the paramodulation active/passive tables to the...
2009-12-09 Andrea AspertiAttached fast_eq_check to auto
2009-12-09 Andrea AspertiAdded nnAuto.mli
2009-12-09 Andrea AspertiDebug set to ()
2009-12-09 Andrea AspertiClean up of debgging info
2009-12-09 Andrea AspertiSyntax error
2009-12-09 Andrea AspertiWrong reference corrected
2009-12-09 Andrea AspertiMinor fixing for last chance
2009-12-09 Andrea AspertiAdded a fol operation
2009-12-04 Wilmer RicciottiBugfix in inversion (was using refl_eq instead of refl).
2009-12-04 Andrea AspertiIndexing local context for paramod.
2009-12-02 Andrea AspertiThe new paramodulation functions instantiated over...
2009-12-02 Andrea AspertiNew ways for initialising the signature required for...
2009-12-02 Andrea AspertiPassive equations have their own index (not passive...
2009-12-02 Andrea Aspertidebug takes lazy strings. Moved here the are_alpha_eq...
2009-12-02 Andrea AspertiAdded a function remove_unit_clause
2009-12-02 Andrea AspertiAdded a boolean test function to discriminate equations...
2009-12-02 Andrea AspertiGeneralized intitialization for EqP
2009-12-02 Andrea AspertiGeneralized initialization of eqP.
2009-11-27 Wilmer Ricciottindestruct now clears off identity equations whenever...
2009-11-25 Wilmer RicciottiFixed inversion, which was broken by the last changes...
2009-11-25 Andrea AspertiExported forward_inference_step
2009-11-24 Wilmer RicciottiBugfix in tipify: a metavariable was set to type withou...
2009-11-24 Wilmer RicciottiIn order to prevent useless meta extensions, we optimiz...
2009-11-24 Wilmer RicciottiWhen unifying
2009-11-23 Andrea AspertiRemoved dead code
2009-11-23 Andrea AspertiSubsumption and reduction
2009-11-19 Wilmer Ricciotti- Added a swap parameter to the unification procedure
2009-11-18 Wilmer RicciottiNCicRefiner.force_to_sort implemented on top of NCicUni...
2009-11-18 Wilmer RicciottiCode factorization for check_type.
2009-11-17 Wilmer Ricciottindestruct tactic: mainly bugfixes; the algorithm isn...
2009-11-17 Andrea AspertiClosing the goal.
2009-11-16 Wilmer RicciottiImplementation of ndestruct tactic (including destructi...
2009-11-13 Andrea AspertiExported apply_subst_context
2009-11-13 Andrea AspertiAdded the new auto version (not attached yet).
2009-11-12 Claudio Sacerdoti... Code made more uniform.
2009-11-10 Andrea AspertiUnion find slightly more general (f can now point to...
2009-11-05 Andrea AspertiA case was missing
2009-11-05 Andrea AspertiNaif version of the union find
2009-11-04 Claudio Sacerdoti... Bug fixed: restrict used to take the list of positions...
2009-11-04 Claudio Sacerdoti... 1) sort computation undone (it used to be bugged anyway)
next