aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:38 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-06 10:08:38 +0000
commitde8cee391af67aafc966c7cde8c3f0c4fff53da3 (patch)
tree3a48e3efb7cbd67212f4869e30bd20dfbedaa994 /plugins/xml
parentf44b80f4b3e512d21653a019583e97b672b55010 (diff)
Adapt pieces of code needing -rectypes
* in Matching and Tacinterp : ad-hoc types for encoding matching result and "next" continuation * in Class_tactics, occurrences of types such as "type t = (foo * (unit->t) option" have been specialized to something like type t = TNone | TSome of foo * (unit -> t) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15869 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml')
0 files changed, 0 insertions, 0 deletions