aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-04 21:29:41 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-08-04 21:29:41 +0000
commitff0a77ae90f39c56e82126978a59d957676e0d9e (patch)
tree89df8f3f9f9c353e5ecede1a75278648baaec4c3 /pretyping/recordops.mli
parent7d515acbc5d83aa2300b71a9b7712b3da1d3d2e3 (diff)
Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par
un nom importé) de la 8.2 vers le trunk. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M pretyping/termops.ml M toplevel/command.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions