Skip to content

Instantly share code, notes, and snippets.

@tomprince

tomprince/gist:856235

Created March 5, 2011 08:37
Show Gist options
  • Save tomprince/856235 to your computer and use it in GitHub Desktop.
Save tomprince/856235 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.ml
Ltac read f :=
match f with
| true => constr :true
| false => constr :false
| _ => constr :tt
end.
Lemma test : true = true.
let v := read true in idtac v.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment