diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /toplevel | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 5 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 2 |
3 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 46b212dee..6788cf1b7 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -198,7 +198,7 @@ let build_id_coercion idf_opt source poly = lams in let typ_f = - it_mkProd_wo_LetIn + List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t)) lams in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index df1f47e33..345eae9df 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1202,6 +1202,7 @@ let explain_recursion_scheme_error = function (* Pattern-matching errors *) let explain_bad_pattern env sigma cstr ty = + let ty = EConstr.to_constr sigma ty in let env = make_all_name_different env in let pt = pr_lconstr_env env sigma ty in let pc = pr_constructor env cstr in @@ -1245,13 +1246,15 @@ let explain_non_exhaustive env pats = spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) let explain_cannot_infer_predicate env sigma typs = + let inj c = EConstr.to_constr sigma c in + let typs = Array.map_to_list (fun (c1, c2) -> (inj c1, inj c2)) typs in let env = make_all_name_different env in let pr_branch (cstr,typ) = let cstr,_ = decompose_app cstr in str "For " ++ pr_lconstr_env env sigma cstr ++ str ": " ++ pr_lconstr_env env sigma typ in str "Unable to unify the types found in the branches:" ++ - spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs)) + spc () ++ hov 0 (prlist_with_sep fnl pr_branch typs) let explain_pattern_matching_error env sigma = function | BadPattern (c,t) -> diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fef99d8af..0723f16c3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -488,7 +488,7 @@ let build_combined_scheme env schemes = let ctx, _ = list_split_rev_at prods (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in - let typ = it_mkProd_wo_LetIn concl_typ ctx in + let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in (body, typ) |