aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-27 14:16:07 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-02-27 14:16:07 +0000
commitceea3d3a9104445584cfd28e47ddda452e87fb66 (patch)
tree5bc4207e100de770d64245a24b1cae071196796c /contrib/extraction
parentd56e6710b232665fbc5e5199a1c7e51f61d8a6fc (diff)
typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/ocaml.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 16859a9c1..f0ae3f264 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -29,7 +29,7 @@ let rec msid_of_mt = function
| MTident mp -> begin
match Modops.eval_struct (Global.env()) (SEBident mp) with
| SEBstruct(msid,_) -> MPself msid
- | _ -> anomaly "Extraction:the With can'tbe applied to a funsig"
+ | _ -> anomaly "Extraction:the With can't be applied to a funsig"
end
| MTwith(mt,_)-> msid_of_mt mt
| _ -> anomaly "Extraction:the With operator isn't applied to a name"