on b8a2bbf help sign in
all commits
de89a04Add ElabInfo to pass through elaboratorEdwin Brady 44d62c7Better if unification substitutes rather than let bindsEdwin Brady ffd5e72arg tactic; unification tweakEdwin Brady cc0dc09Added elaborate; a language for composing primitive tactics.Edwin Brady cbc60ebUnification, and unify tacticEdwin Brady 6a6a048No mucking about with de Bruijn indices in proof constructionEdwin Brady 205fcefSome proof state, some showing of termsEdwin Brady dc0c198First lot of source files and paperEdwin Brady