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.04Feb32131Jan2928272625242221201817161512987643220Dec19181615141312109826Nov252422211817158124Oct2320191815141211109527Sep25242320174331Aug3015Jul29Jun25May201917Mar1619Feb719Jan16Dec1454130Nov282731Oct30282019119229Sep2524Jul87121Jun20173227May26221817141127Apr2322212017151413129876432130Mar242321171211109543228Feb272624212017231Jan30291613818Nov25Oct24Systematically 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 ElMerge branch 'devel' into lp2There may be no actualsMerge branch 'devel' into lp2Get systematically actualsMerge branch 'devel' into lp2Fix tuple printing (less metavariables)Proof exportDo not handle errorsupdate testsBetter propositional quantificationQuantification macro, optional stream for abstractMerge branch 'devel'Removed nonsens