]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/cic_omdoc
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
ocaml 3.09 transition
[helm.git] / helm / ocaml / cic_omdoc /
2005-11-22 Stefano Zacchiroli- more resilient to proof checking failures during... tree | commitdiff
2005-11-22 Stefano Zacchirolibugfix: return unshared sequent when applying cic ... tree | commitdiff
2005-11-07 Claudio Sacerdoti... Let-ins with types can be produced. tree | commitdiff
2005-09-23 Enrico Tassiadded universes tree | commitdiff
2005-09-21 Claudio Sacerdoti... We do not longer generate inner-types and inner-sorts... tree | commitdiff
2005-09-07 Claudio Sacerdoti... Unsharing bugs fixed. tree | commitdiff
2005-09-07 Claudio Sacerdoti... Unsharing bug due to a very stupid typo fixed. tree | commitdiff
2005-09-06 Claudio Sacerdoti... Dead code/files removed. tree | commitdiff
2005-09-06 Claudio Sacerdoti... Serious bug fixed: unsharing was not performed over... tree | commitdiff
2005-09-06 Claudio Sacerdoti... Dead code removed. tree | commitdiff
2005-09-02 Claudio Sacerdoti... Unsharing finally introduced (but just for object proce... tree | commitdiff
2005-09-02 Claudio Sacerdoti... Assert added to check whether an unsharing problem... tree | commitdiff
2005-07-25 Stefano Zacchiroliimplemented transformations on top of notation code tree | commitdiff
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri tree | commitdiff
2005-06-10 Claudio Sacerdoti... head_beta_reduce used to create applications of applica... tree | commitdiff
2005-05-31 Stefano ZacchiroliChanged type of ids_to_inner_sort table used in transfo... tree | commitdiff
2005-05-18 Enrico Tassifixed some TODO in content2pres tree | commitdiff
2005-05-03 Enrico Tassiadded sqlStatements module (contains all CREATE TABLE... tree | commitdiff
2005-04-27 Stefano Zacchirolimerged changes from the svn fork by me and Enrico tree | commitdiff
2005-03-09 Stefano Zacchiroliadded support for open terms in check tree | commitdiff
2005-02-04 Stefano Zacchiroliremoved dep on mathql tree | commitdiff
2005-02-02 Stefano Zacchiroliadded inductive_name field to inductive definitions... tree | commitdiff
2005-01-21 Stefano Zacchiroliadded attributes tree | commitdiff
2005-01-20 Stefano Zacchiroli- added rendering of constants/variable with/without... tree | commitdiff
2005-01-17 Enrico Tassinew cicEnvironment implementation tree | commitdiff
2004-12-01 Enrico TassiAdded universes handling. The PRE_UNIVERSES tag may... tree | commitdiff
2004-11-25 Stefano Zacchiroliprotected invocations to get_cooked_obj with assertion... tree | commitdiff
2004-11-10 Stefano Zacchirolicommented out some timing messages tree | commitdiff
2004-10-22 Stefano Zacchirolino longer depends on MQueryMisc tree | commitdiff
2004-07-01 Stefano ZacchiroliNew handling of substitution: tree | commitdiff
2004-04-23 Enrico TassiUniverses introduction tree | commitdiff
2004-04-19 Stefano Zacchirolifixed a typo (inside a comment) tree | commitdiff
2004-04-15 Andrea AspertiMetasenv added as parameter to eta_fixing. tree | commitdiff
2004-04-06 Stefano Zacchirolieta_fixing of the CurrentProof metasenv is wrong, since... tree | commitdiff
2004-02-24 Claudio Sacerdoti... Partial porting to V8 URIs. tree | commitdiff
2004-02-17 Claudio Sacerdoti... - double_type_of: sort_of_prod modified to expect also... tree | commitdiff
2004-02-10 Claudio Sacerdoti... Only applications whose head was a constant were eta... tree | commitdiff
2004-02-09 Claudio Sacerdoti... Added flag ?eta_fix:bool to acic_object_of_cic_object. tree | commitdiff
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit tree | commitdiff
2004-02-06 Andrea AspertiBug MutCase fixed: now the type of the constructor... tree | commitdiff
2004-02-05 Claudio Sacerdoti... NameExpected exception removed. The "identifier" __n... tree | commitdiff
2004-01-22 Andrea AspertiA few modifications, here and there... tree | commitdiff
2003-12-02 Ferruccio Guidisort CProp added tree | commitdiff
2003-10-07 Luca Padovani* removed currified constructors everywhere. A bug... tree | commitdiff
2003-09-23 Ferruccio Guidipatch tree | commitdiff
2003-09-23 Claudio Sacerdoti... Reindentation tree | commitdiff
2003-09-05 Stefano ZacchiroliDefs in context may now have an optional type (when... tree | commitdiff
2003-09-05 Claudio Sacerdoti... string ==> id tree | commitdiff
2003-09-05 Stefano ZacchiroliDefs in context may now have an optional type (when... tree | commitdiff
2003-09-05 Claudio Sacerdoti... Debugging infos removed. tree | commitdiff
2003-09-05 Claudio Sacerdoti... string => id tree | commitdiff
2003-09-05 Claudio Sacerdoti... Defs in context may now have an optional type (when... tree | commitdiff
2003-07-30 Claudio Sacerdoti... Unuseful id removed from hypothesis. tree | commitdiff
2003-07-30 Andrea AspertiEta fixing for MTCases added (that meant to recursively... tree | commitdiff
2003-07-30 Claudio Sacerdoti... All the ids are now generated by gen_id. (Some of them... tree | commitdiff
2003-07-29 Andrea AspertiAdded method "FalseInd". tree | commitdiff
2003-07-29 Claudio Sacerdoti... Prefixes introduced for the generated ids/xrefs. Example: tree | commitdiff
2003-07-29 Andrea AspertiAdded method AndInd. tree | commitdiff
2003-07-28 Andrea AspertiFew modif in eta-fixing. tree | commitdiff
2003-07-25 Claudio Sacerdoti... Lemma generated wrong URIs (again). Fixed. tree | commitdiff
2003-07-24 Andrea AspertiComplete beta reduction added to avoid strange case... tree | commitdiff
2003-07-24 Andrea AspertiThe name of TD proofs was erroneously always set to... tree | commitdiff
2003-07-23 Andrea Asperti- Lemma added to the list of proof arguments tree | commitdiff
2003-07-21 Andrea AspertiThe Aux argument of conclude is now of type string... tree | commitdiff
2003-07-21 Claudio Sacerdoti... Interface change: only cobj2obj is exposed. tree | commitdiff
2003-07-21 Claudio Sacerdoti... Flattening application contexts uncorrectly changed... tree | commitdiff
2003-07-21 Andrea Asperti** UNTESTED ** tree | commitdiff
2003-07-21 Andrea AspertiWe do not compute inner-types for the metasenv ==>... tree | commitdiff
2003-07-20 Claudio Sacerdoti... Reindenting. tree | commitdiff
2003-07-20 Claudio Sacerdoti... proof2cic now uses Deannotate.deannoate_term instead... tree | commitdiff
2003-07-20 Claudio Sacerdoti... Cic2acic is now responsible of eta-fixing the objects... tree | commitdiff
2003-07-20 Claudio Sacerdoti... cic2content.ml* moved from cic_transformations to cic_o... tree | commitdiff
2003-07-20 Claudio Sacerdoti... Content2cic e Eta_fixing moved from gTopLevel to cic_omdoc. tree | commitdiff
2003-07-20 Claudio Sacerdoti... ... tree | commitdiff
2003-07-20 Claudio Sacerdoti... cic_transformations factorized into cic_omdoc and cic_t... tree | commitdiff
Unnamed repository; edit this file 'description' to name the repository.