aboutsummaryrefslogtreecommitdiff
path: root/pretyping/cbv.ml
diff options
context:
space:
mode:
authorJPR2019-05-23 23:28:55 +0200
committerJPR2019-05-23 23:28:55 +0200
commitd306f5428db0d034aea55d3f0699c67c1f296cc1 (patch)
tree540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /pretyping/cbv.ml
parent5cfdc20560392c2125dbcee31cfd308d5346b428 (diff)
Fixing typos - Part 3
Diffstat (limited to 'pretyping/cbv.ml')
-rw-r--r--pretyping/cbv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 5ea9b79336..4aa55e4d0d 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -477,7 +477,7 @@ and cbv_stack_value info env = function
cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk)
| Some v -> cbv_stack_value info env (v,stk)
| None -> mkSTACK(PRIMITIVE(op,c,args), stk)
- else (* partical application *)
+ else (* partial application *)
(assert (stk = TOP);
PRIMITIVE(op,c,appl))