diff options
| author | ppedrot | 2012-11-22 18:09:55 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-22 18:09:55 +0000 |
| commit | e363a1929d9a57643ac4b947cfafbb65bfd878cd (patch) | |
| tree | f319f1e118b2481b38986c1ed531677ed428edca /pretyping/patternops.ml | |
| parent | 2e43b03b0bb88bd3b4cb7695d5079c51ca41b0a7 (diff) | |
Monomorphization (pretyping)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 1f16385a62..bd08df5334 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -134,7 +134,10 @@ let map_pattern_with_binders g f l = function | PFix _ | PCoFix _ as x) -> x let error_instantiate_pattern id l = - let is = if List.length l = 1 then "is" else "are" in + let is = match l with + | [_] -> "is" + | _ -> "are" + in errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") @@ -326,8 +329,11 @@ and pats_of_glob_branches loc metas vars ind brs = | [] -> false, [] | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs -> - if ind <> None && ind <> Some indsp then - err loc (Pp.str "All constructors must be in the same inductive type."); + let () = match ind with + | Some sp when eq_ind sp indsp -> () + | _ -> + err loc (Pp.str "All constructors must be in the same inductive type.") + in if Intset.mem (j-1) indexes then err loc (str "No unique branch for " ++ int j ++ str"-th constructor."); |