diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /vernac/comFixpoint.ml | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 00f19f545c..a428c42e49 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -333,7 +333,7 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na | CMeasureRec (None,_,_) when not structonly -> - user_err Pp.(str "Decreasing argument must be specificed in measure clause.") + user_err Pp.(str "Decreasing argument must be specified in measure clause.") | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") |