]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
added simplify to avoid ugly proofterm
[helm.git] / helm / software / components /
2008-04-07 Claudio Sacerdoti... Tentative (and bad!) fix of outtypes in non-dependent...
2008-04-07 Claudio Sacerdoti... Cooking discriminated into cooking in types (using...
2008-04-07 Claudio Sacerdoti... Pretty-printing of definitions fixed.
2008-04-07 Claudio Sacerdoti... Cooking implemented (not tested yet).
2008-04-07 Claudio Sacerdoti... Reports improved.
2008-04-07 Claudio Sacerdoti... Debugging code fixed.
2008-04-07 Enrico Tassiadded invalidate to clear the cache and ease the compar...
2008-04-07 Enrico Tassicommented out uris of objs that do not compile properly
2008-04-07 Enrico Tassiadded comparison with old kernel
2008-04-07 Enrico Tassifixed error message for eat prods
2008-04-07 Enrico Tassiinvalidate
2008-04-07 Enrico Tassiuris relative to axioms are translated in the right way
2008-04-07 Enrico Tassiadded invalidate
2008-04-07 Enrico Tassiadded preliminary checks for indtys
2008-04-07 Enrico Tassicall get_obj instead of get_cooked_obj ~trust:false
2008-04-07 Enrico Tassiadded case of const and axiom
2008-04-07 Enrico Tassiadded # to comment
2008-04-07 Enrico Tassibetter printings
2008-04-07 Enrico Tassithe explicit type in a LetIn must be typecheckd before...
2008-04-07 Enrico Tassiopt compilation enabled, removed some pps, check has...
2008-04-07 Enrico Tassilefts_ad_tys properly sorted, added some metasenv here...
2008-04-07 Enrico Tassilefts_and_tys was tys@lefts, CSC claims it was working...
2008-04-07 Enrico Tassiadded a list of uris to ease debugging
2008-04-07 Enrico Tassiprint the excpetion and raise it again, seems to produc...
2008-04-07 Enrico Tassinew constants have depth = max_int insted of 0 so that...
2008-04-07 Enrico Tassioff by one in calling count_from
2008-04-07 Enrico Tassifixed bug in translating Fix, recno was not properly...
2008-04-07 Enrico Tassiadded a pretty printing of the new object and use argv...
2008-04-07 Enrico Tassicontext, metasenv and subst made mandatory in CicPp
2008-04-07 Enrico Tassiguarded by has a nice error message
2008-04-07 Enrico Tassireference type made private, added mk_constructor to...
2008-04-04 Enrico Tassisome debug printings
2008-04-04 Enrico Tassiadded to the cache a boolean to state if the object is
2008-04-04 Enrico Tassifix
2008-04-04 Enrico Tassitoday it seems that the substituted should be lifted...
2008-04-04 Enrico Tassiadded ppobj
2008-04-04 Enrico Tassitype_of_constant was retunrning the type of the wrong...
2008-04-04 Enrico Tassifixed list.nth and added some paretheses
2008-04-04 Enrico Tassiadded some printings and catched more exceptions
2008-04-04 Enrico Tassiremoved useless printing
2008-04-04 Enrico Tassiiterator map was mapping Lambdas to Prods!!!
2008-04-04 Enrico Tassidebugging started
2008-04-04 Enrico Tassitype of constant ported
2008-04-04 Enrico Tassiadded add_obj to store objects in the environment,...
2008-04-04 Enrico Tassilogger added
2008-04-04 Enrico Tassiadded get_obj in nCicEnvironment that returns an object...
2008-04-04 Enrico Tassiindentation fixed
2008-04-04 Enrico Tassireturns_a_counductive implemented
2008-04-04 Enrico Tassitype_of_branch ported and optimized to not lift the...
2008-04-04 Enrico Tassiis_really_smaller ported, still to understand the case...
2008-04-03 Enrico Tassidebujin implemented with the map recursor
2008-04-03 Enrico Tassibug found rewriting the kernel backported: n instead...
2008-04-03 Enrico Tassinon debruijned constructor may be useless elswere,...
2008-04-03 Enrico Tassiguarded_by_destructor ported, many auxiliary functions...
2008-04-03 Enrico Tassiremoved FSF banner
2008-04-02 Enrico Tassiadded slim version of does_not_occur
2008-04-02 Enrico Tassiadded translation of Set to Type0 (avoid warning)
2008-04-02 Enrico Tassifixes backported from the new kernel
2008-04-01 Enrico Tassibetter check for progress
2008-04-01 Claudio Sacerdoti... typeof_obj0 implemented
2008-04-01 Claudio Sacerdoti... 1) added get_checked_indtys that returns the whole...
2008-04-01 Enrico Tassiprogress made better, still not perfect
2008-04-01 Enrico Tassiadded to rewrite a check to effectively do something...
2008-04-01 Enrico Tassiadded some comments, but the samentics of many function...
2008-04-01 Enrico Tassiadded set_ppterm
2008-03-31 Claudio Sacerdoti... Automatic generation of elimination and inversion princ...
2008-03-31 Claudio Sacerdoti... Large amount of duplicated code (still in comments...
2008-03-31 Claudio Sacerdoti... 1) Impredicative sort "Set" removed everywhere.
2008-03-31 Claudio Sacerdoti... 1) more sharing everywhere in NCicSubstitution
2008-03-27 Enrico Tassimore cases of the type checker honoured, still missing...
2008-03-27 Enrico Tassiadded is_closed to nCicUtils.
2008-03-27 Enrico Tassimoved psubst and list to the new iterators, result...
2008-03-27 Enrico Tassiadded iterators over NCic terms
2008-03-27 Enrico Tassiremoved FSF header
2008-03-27 Enrico Tassiinsert comments of old tpechecker
2008-03-25 Enrico Tassinew are_convertible and head_beta_reduce
2008-03-25 Enrico Tassicontext for fixpoint body created in the hopefully...
2008-03-25 Enrico Tassiported to the Cic LetIn with explicit type
2008-03-25 Enrico Tassithis patch is a shit, the part that fixes the heuristic...
2008-03-25 Enrico TassiXXX this is the beginning of the metaocaml work XXX
2008-03-23 Ferruccio GuidicicNotationPp: fixed letin syntax (now typeless)
2008-03-20 Enrico Tassichanged auto_tac params type and all derivate tactics...
2008-03-20 Claudio Sacerdoti... End of patch for computation of LetIn types. Now types...
2008-03-19 Claudio Sacerdoti... Bug: types and terms pushed into the context must be...
2008-03-19 Claudio Sacerdoti... prerr_endline => debug_print
2008-03-19 Claudio Sacerdoti... prerr_endline => debug_print
2008-03-19 Claudio Sacerdoti... Number notation for Coq is back again, waiting for...
2008-03-19 Ferruccio GuidiProcedural : added some missing cases
2008-03-18 Ferruccio GuidiProcedural : tentative update to the new letin cic...
2008-03-13 Claudio Sacerdoti... :-(
2008-03-12 Claudio Sacerdoti... Almost always correct optimization: during unification...
2008-03-12 Enrico Tassifixed implicit
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-10 Claudio Sacerdoti... Bad hack to avoid failure of conversion (unfolding...
2008-03-10 Claudio Sacerdoti... ...
2008-03-10 Claudio Sacerdoti... Tactic reduce got rid of. Use normalize, instead.
2008-03-10 Claudio Sacerdoti... whd: ~delta=false now controls also zeta-reduction...
2008-03-10 Claudio Sacerdoti... An unimplemented case of clearbody is now implemented.
2008-03-10 Claudio Sacerdoti... check_metasenv_consistency:
2008-03-10 Claudio Sacerdoti... Debugging print removed.
next