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