]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2004-02-06 Stefano Zacchiroliadded -g flag to ocamlc per default
2004-02-06 Stefano Zacchirolitextual term editor is now the default one
2004-02-06 Stefano Zacchiroliignore .debug_script (used by Makefile's debug target)
2004-02-06 Stefano Zacchiroli- split regtest/testlibrary/gTopLevel objects so that...
2004-02-06 Andrea AspertiBug MutCase fixed: now the type of the constructor...
2004-02-06 Stefano Zacchiroliadded testlibrary.opt and some cm****
2004-02-05 Claudio Sacerdoti... NameExpected exception removed. The "identifier" __n...
2004-02-05 Claudio Sacerdoti... Improved error messages.
2004-02-05 Claudio Sacerdoti... No more garbage in the metasenv.
2004-02-05 Claudio Sacerdoti... New target librarytest (to apply testlibrary.opt to...
2004-02-05 Stefano Zacchiroli- added support for multiple choices
2004-02-05 Stefano Zacchirolibetter output format
2004-02-05 Stefano Zacchiroliflush stdout after print_string
2004-02-05 Stefano Zacchirolidebug prints on stderr
2004-02-05 Stefano Zacchiroliremoved duplicated entry about freshNamesGenerator
2004-02-05 Stefano Zacchiroli- added testlibrary .opts
2004-02-05 Stefano Zacchiroliadded \to notation for anonymous binders Pi and Lambda
2004-02-05 Stefano Zacchirolibugfix: use rev_uniq also on non-located term
2004-02-05 Claudio Sacerdoti... sort_of_prod relaxed to accept also Metas (when the...
2004-02-05 Claudio Sacerdoti... - sort_of_prod now returns the second Meta (if it is...
2004-02-05 Stefano Zacchiroliadded html_of_html_msg
2004-02-05 Claudio Sacerdoti... __n no longer generated.
2004-02-05 Claudio Sacerdoti... "assert false" relaxed to a warning.
2004-02-05 Claudio Sacerdoti... No longer puts anonymous declarations in the canonical...
2004-02-05 Claudio Sacerdoti... - the result of a refinement is now cleared from dummy...
2004-02-05 Claudio Sacerdoti... freshNameGenerator.ml* added
2004-02-05 Stefano Zacchirolirebuilt
2004-02-05 Stefano Zacchiroliadded freshNameGenerator
2004-02-05 Stefano Zacchiroliadded testlibrary script
2004-02-05 Stefano Zacchiroliuse a dummy location when no location is provided
2004-02-05 Stefano Zacchiroliadded ( ) notation for binders
2004-02-05 Claudio Sacerdoti... dummy dependent types and dummy letins are now removed...
2004-02-05 Claudio Sacerdoti... fresh_name_generator has now also the metasenv parameter.
2004-02-05 Claudio Sacerdoti... mk_fresh_name moved to FreshNamesGenerator.
2004-02-05 Claudio Sacerdoti... New test.
2004-02-05 Claudio Sacerdoti... Final answer: the local context MUST be normalized...
2004-02-05 Claudio Sacerdoti... Restrict reimplemented to avoid generating lists of...
2004-02-05 Claudio Sacerdoti... Added a TODO (to catch only the right exceptions instea...
2004-02-05 Claudio Sacerdoti... Bug fixed: the canonical contexts were traversed in...
2004-02-04 Claudio Sacerdoti... Rel to hidden hypotheses are now printed as _hidden_n.
2004-02-04 Claudio Sacerdoti... ppterm_in_context exported
2004-02-04 Claudio Sacerdoti... ppcontext (and thus also ppmetasenv) were buggy: the...
2004-02-04 Claudio Sacerdoti... Functors must be applied using parentheses around the...
2004-02-04 Claudio Sacerdoti... Added newline.
2004-02-04 Claudio Sacerdoti... Bug fixed: restriction of already restricted contexts...
2004-02-04 Claudio Sacerdoti... Effects of fixing bugs for other regression tests ;-)
2004-02-04 Claudio Sacerdoti... We no longer apply the subst to a Meta in force_does_no...
2004-02-04 Andrea Aspertidelift no longer apply the substitution when a Meta...
2004-02-04 Andrea AspertiAdded a new example.
2004-02-04 Claudio Sacerdoti... ...
2004-02-04 Claudio Sacerdoti... report files are now produced (and removed) during...
2004-02-04 Claudio Sacerdoti... Patch to delift withdrawn.
2004-02-04 Claudio Sacerdoti... ...
2004-02-04 Claudio Sacerdoti... Typo fixed. Used to break target gentest.
2004-02-04 Claudio Sacerdoti... Bug fixed: when a variable not instantiated yet was...
2004-02-04 Claudio Sacerdoti... Improved regression testing reporting.
2004-02-04 Claudio Sacerdoti... - regtest: better argument handling (using Arg)
2004-02-04 Stefano Zacchiroliremoved a debugging message
2004-02-04 Stefano Zacchiroli- improved some error messages
2004-02-04 Stefano Zacchirolimoved here CicAst and pretty printer
2004-02-04 Stefano Zacchiroliported to CicAst
2004-02-04 Stefano Zacchiroli- sorted domain which hopefully avoids exponential...
2004-02-04 Stefano Zacchirolimoved Ast in cic_transformations/
2004-02-04 Stefano Zacchiroli- added support for implicit in concrete syntax
2004-02-03 Claudio Sacerdoti... regression tests
2004-02-03 Claudio Sacerdoti... cic_mkimplicit' removed (its implementation was wrong...
2004-02-03 Claudio Sacerdoti... Debugging code removed.
2004-02-03 Claudio Sacerdoti... sort_of_prod changed to not generate a new metavariable...
2004-02-03 Stefano Zacchiroli- comment inside .test file that explain what follows
2004-02-03 Stefano Zacchiroliadded cleantest target (removes tests/*.test)
2004-02-03 Claudio Sacerdoti... Check missed: the two metasenv were not compared.
2004-02-03 Claudio Sacerdoti... Debuggin infos removed.
2004-02-03 Claudio Sacerdoti... - do not crash any longer if type-checking or reduction...
2004-02-03 Claudio Sacerdoti... time added to regtest
2004-02-03 Stefano Zacchirolicatch just AssertFailure instead of _ (AssertFailure...
2004-02-03 Stefano Zacchiroliremoved SortExpectedMetaFound special exception
2004-02-03 Stefano Zacchiroliadded urimanager dependency
2004-02-03 Claudio Sacerdoti... Meta vs same Meta now tries unification when convertibi...
2004-02-03 Stefano Zacchirolis/LocatedTerm/AnnotatedTerm + various annotations/
2004-02-03 Claudio Sacerdoti... New tests for lambdas (that show bugs in applications ;-)
2004-02-03 Stefano Zacchirolicatch exceptions and mark corresponding tests as failed
2004-02-03 Claudio Sacerdoti... eat_prods reimplemented to generalize the output type...
2004-02-03 Claudio Sacerdoti... Added an optional parameter to identity_relocation_list...
2004-02-03 Claudio Sacerdoti... More debug informations.
2004-02-02 Claudio Sacerdoti... Substitution no longer returned from CicRefine.type_of_aux
2004-02-02 Stefano Zacchiroliported to new type_of prototype
2004-02-02 Stefano Zacchiroliuses CicMetaSubst.ppterm where needed
2004-02-02 Stefano Zacchiroli- refine's type_of no longer return a substitution
2004-02-02 Stefano Zacchiroliported to latest Ast changes (mainly capture_variable...
2004-02-02 Stefano Zacchiroli- added entries for capture variables parsing
2004-02-02 Stefano Zacchiroli- added capture_variable entry and Cic.names here and...
2004-02-02 Stefano Zacchiroli- changed ast for pattern matching so that type annotat...
2004-02-02 Stefano Zacchiroli- big hack: keep on unifying/refining when SortExpected...
2004-02-02 Stefano Zacchiroli- removed metasenv argument from kernel proxies invocations
2004-02-02 Stefano Zacchiroli- added SortExpectedMetaFound exception (huge hack)
2004-02-02 Stefano Zacchiroli- bugfix for expand_implicits, return correct term...
2004-02-02 Stefano Zacchiroli- removed unwind: every substitution is now _not_ unwinded
2004-02-02 Stefano Zacchirolichanged prototype of CicMetaSubst.apply_subst*
2004-02-02 Stefano Zacchiroliadded comments
2004-02-02 Stefano Zacchirolifact regtest
next