diff options
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.") |