Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
1 result
You can move around the graph by using the arrow keys.
Created with Raphaël 2.2.022Jun1410Feb5432131Jan2928272625242221201817161512987643220Dec19181615141312109826Nov252422211817158124Oct2320191815141211109527Sep25242320174331Aug3015Jul29Jun25May201917Mar1619Feb719Jan16Dec1454130Nov282731Oct30282019119229Sep2524Jul87121Jun20173227May26221817141127Apr2322212017151413129876432130Mar242321171211109543228Feb272624212017231Jan30291613818Nov25Oct24Revert "Try to typecheck real_defs"Make runtest exit with output 1 when test failsFixed telescopesTry to typecheck real_defsupdating CIadd option to only translate preludeMerge branch 'devel'Prepare release 0.1Merge branch 'devel'Add lisp testing for preludeProper test for translatorSome notes, cast functionUpdated translatable theoriesSystematically get the supertype of expr-as-typeUpdate forbidden lettersRe introducing opacitySlightly simpler formal handlingDon't store theory bindingsNo need for *ctx*Improvements over bindingsAllow abstract-over to take single elementsBetter pprint formalsHandle full fledged telescopesDocumentationLisp testingDynamically bind global variables in pp-dkMore lisp for tests, prelude as a testMerge branch 'lp2' into develUpdating proof toolsAdapting json to new typecheckingCI nitpicksExpliciting coercion rulesUse SBCL for common tasksprelude check does not need psnj anymoreMerge branch 'devel' into lp2fix testsUpdating CIHack for non provided subtyping proofsUse lisp to parse theory specificationsFixed coercions: no need to match on El