Skip to content
Snippets Groups Projects

Repository graph

You can move around the graph by using the arrow keys.
Select Git revision
  • master default protected
1 result
Created with Raphaël 2.2.015Jul14135428Jun272524212016151311107643230May18171310428Apr128Mar2726109822Feb134328Jan2521201918update READMEmastermasterupdate levels of headingsupdate READMEupdate READMErearrange BinaryTypedrearrange Common/Unary/Binarymove makefile, add build instructionscomments in BinaryTyped/LogRel.vcomments in BinaryTyped/Compatibility.vcomments in BinaryTyped/WeakSub.vcomments in BinaryTyped/SyntacticMinimalInvariance.vcomments in BinaryTyped/LogRel.v and BinaryTyped/WeakSub.vComments in unary and binary branch.fix some comments in Language.v, Lib.v and Unary, simplify two proofschange associativity of /\ in def. of logrel (BinaryTyped)update dependencies.pngmove definition of contexts to Language.v/Lib.v,remove duplicate lemma, add other direction in Queues.vcleanup DeBruijn.v, update dependencies.gvcleanupfinish SyntacticMinimalInvariance.v (still needs cleanup)some cleanupadd file Tactics.v improve proofs in queue exampleadd proofs for two substitution lemmasmove notation for empty context to central locationSyntacticMinimalInvariance.v : first version of proof (still with someadd BinaryTyped.Soundness.v, beginfinish BinaryTyped/Compatibility.vBinaryTyped/Compatibility.v: compat lemmas through casetype subst for environments, working version of ext_substsimplify definition of T_t1, T_t2. BinaryTyped/WeakSub.vadd types into evaluation closure, change eval_simpl, add preservationBinaryTyped.WeakSub.vsyntactic weakening and substitutiondblib: add lemmas subst_insert, lookup_liftfix Binary/Soundness.vbinarytyped -> BinaryTyped, add _CoqProject fileBinary.Compatibility.v: clean up code, add documentationupdate Makefilechange environments of pairs to pairs of environments