| 2008-04-09 |
Enrico Tassi | pp with parenthesis only when necessary and with some...
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | better pp in Appl
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | better pp
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | pretty printer on steroids
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | added profiling on/off
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | invalidate fixed
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | allow to switch profiling on and off on the fly
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still...
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-04-08 |
Enrico Tassi | added simplify to avoid ugly proofterm
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added invalidate to clear the cache and ease the comparison...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | commented out uris of objs that do not compile properly
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added comparison with old kernel
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | fixed error message for eat prods
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | invalidate
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | uris relative to axioms are translated in the right way
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added invalidate
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added preliminary checks for indtys
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | call get_obj instead of get_cooked_obj ~trust:false
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added case of const and axiom
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added # to comment
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | better printings
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | the explicit type in a LetIn must be typecheckd before...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | opt compilation enabled, removed some pps, check has...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | lefts_ad_tys properly sorted, added some metasenv here...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | lefts_and_tys was tys@lefts, CSC claims it was working...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added a list of uris to ease debugging
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | print the excpetion and raise it again, seems to produce...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | new constants have depth = max_int insted of 0 so that...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | off by one in calling count_from
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | fixed bug in translating Fix, recno was not properly...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added a pretty printing of the new object and use argv...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | context, metasenv and subst made mandatory in CicPp
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | guarded by has a nice error message
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | reference type made private, added mk_constructor to...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | some debug printings
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | added to the cache a boolean to state if the object is
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | fix
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | today it seems that the substituted should be lifted...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | added ppobj
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | type_of_constant was retunrning the type of the wrong...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | fixed list.nth and added some paretheses
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | added some printings and catched more exceptions
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | removed useless printing
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | iterator map was mapping Lambdas to Prods!!!
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | debugging started
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | type of constant ported
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | added add_obj to store objects in the environment,...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | logger added
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | added get_obj in nCicEnvironment that returns an object...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | indentation fixed
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | returns_a_counductive implemented
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | type_of_branch ported and optimized to not lift the...
|
commit | commitdiff | tree |
| 2008-04-04 |
Enrico Tassi | is_really_smaller ported, still to understand the case...
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | debujin implemented with the map recursor
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | bug found rewriting the kernel backported: n instead...
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | non debruijned constructor may be useless elswere,...
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | guarded_by_destructor ported, many auxiliary functions...
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | removed FSF banner
|
commit | commitdiff | tree |
| 2008-04-03 |
Enrico Tassi | added ugly test showing many many bugs in the current...
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | added slim version of does_not_occur
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | added translation of Set to Type0 (avoid warning)
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixes backported from the new kernel
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrites
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixed according to the new rewrite semantics (fails...
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixed depends after the removal of Fsub
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | better check for progress
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | progress made better, still not perfect
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added to rewrite a check to effectively do something...
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added some comments, but the samentics of many functions...
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added set_ppterm
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | more cases of the type checker honoured, still missing...
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | added is_closed to nCicUtils.
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | moved psubst and list to the new iterators, result...
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | added iterators over NCic terms
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | removed FSF header
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | insert comments of old tpechecker
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | new are_convertible and head_beta_reduce
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | context for fixpoint body created in the hopefully...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | ported to the Cic LetIn with explicit type
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | this patch is a shit, the part that fixes the heuristic...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | fix with m (to be optimized) are rewritten such that...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | very very interesting hack
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | argument of type mcu_type always abstracted first
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | XXX this is the beginning of the metaocaml work XXX
|
commit | commitdiff | tree |
| 2008-03-23 |
Enrico Tassi | Fsub moved in contribs
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | since many stuff is under contrib, we need to ignore...
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | library_auto moved inside contrib, still not ported...
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | moved dama/ and dama_didactic/ in contribs/dama/
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | freescale moved under contribs. contribs made relocatable
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics...
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | new semantics for 'by t'
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | removed pointless test
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | I believe that auto paramodulation does not try to
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | added library option to auto
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | letins are no more unfolded, we do that by hand
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | letin are no longer unfolded thus coercions not propagated...
|
commit | commitdiff | tree |
| 2008-03-12 |
Enrico Tassi | fixed implicit
|
commit | commitdiff | tree |
| next |
projects / helm.git / search