aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/decls.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-02 10:28:16 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-02 10:36:16 +0100
commit292e205138ca11c3dce37d48cb34ef4172f6fa06 (patch)
tree904400cafe379136a0e65f026ae9a45c743e4ca0 /library/decls.ml
parente93b9402823cbb9d4713974c51b89d77a7f83b95 (diff)
Removing a source of type-unsafeness in Pcoq.
Diffstat (limited to 'library/decls.ml')
0 files changed, 0 insertions, 0 deletions