diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-22 15:31:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-23 12:09:14 +0200 |
| commit | 74ddca99c649f2f8c203582a9b82bddf64fb6b52 (patch) | |
| tree | f23aa6340c2630619864666ef5eed257d3d765d9 /toplevel/himsg.ml | |
| parent | d23c7539887366202bc370d0f80c26a557486e1c (diff) | |
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b2f752dce..fd74f9c06 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1064,23 +1064,6 @@ let explain_wrong_numarg_inductive env ind n = str "The inductive type " ++ pr_inductive env ind ++ str " expects " ++ str (decline_string n "argument") ++ str "." -let explain_wrong_predicate_arity env pred nondep_arity dep_arity= - let env = make_all_name_different env in - let pp = pr_lconstr_env env pred in - str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++ - str "should be of arity" ++ spc () ++ - pr_lconstr_env env nondep_arity ++ spc () ++ - str "(for non dependent case) or" ++ - spc () ++ pr_lconstr_env env dep_arity ++ spc () ++ - str "(for dependent case)." - -let explain_needs_inversion env x t = - let env = make_all_name_different env in - let px = pr_lconstr_env env x in - let pt = pr_lconstr_env env t in - str "Sorry, I need inversion to compile pattern matching on term " ++ - px ++ str " of type: " ++ pt ++ str "." - let explain_unused_clause env pats = (* Without localisation let s = if List.length pats > 1 then "s" else "" in @@ -1112,10 +1095,6 @@ let explain_pattern_matching_error env = function explain_wrong_numarg_constructor env c n | WrongNumargInductive (c,n) -> explain_wrong_numarg_inductive env c n - | WrongPredicateArity (pred,n,dep) -> - explain_wrong_predicate_arity env pred n dep - | NeedsInversion (x,t) -> - explain_needs_inversion env x t | UnusedClause tms -> explain_unused_clause env tms | NonExhaustive tms -> |