diff options
| author | msozeau | 2011-03-11 17:00:35 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-11 17:00:35 +0000 |
| commit | 7a97fcc78a73ab36d0cb1526397b4d2d7299ed34 (patch) | |
| tree | eadfc5720feb5b443e771b81adbfc2645d411ac4 /toplevel | |
| parent | 36b8aa6b0a6302e1675df623bf28e86029bb40f5 (diff) | |
- Better error messages taking unif. constraints into account.
- Normalize evars in typeclasses eauto also before [intro].
- Disallow use of nf_evars variants that drop unif. constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13904 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/autoinstance.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 8 |
2 files changed, 6 insertions, 4 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 242a8e52b4..af1330a42b 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -255,7 +255,7 @@ let gen_sort_topo l evm = (* register real typeclass instance given a totally defined evd *) let declare_instance (k:global_reference -> rel_context -> constr list -> unit) (cl,gen,evm:signature) = - let evm = Evarutil.nf_evars evm in + let evm = Evarutil.nf_evar_map evm in let gen = gen_sort_topo gen evm in let (evm,gen) = List.fold_right (fun ev (evm,gen) -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6af1f9d56c..60a3b89bb0 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -696,7 +696,7 @@ let explain_no_instance env (_,id) l = prlist_with_sep pr_spc (pr_lconstr_env env) l let pr_constraints printenv env evm = - let evm = Evarutil.nf_evars_undefined evm in + let evm = Evarutil.nf_evar_map_undefined evm in let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -706,12 +706,14 @@ let pr_constraints printenv env evm = (reset_with_named_context evi.evar_hyps env) in (if printenv then pe ++ fnl () else mt ()) ++ prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l + (fun (ev, evi) -> str(string_of_existential ev) ++ + str " : " ++ pr_lconstr evi.evar_concl) l ++ fnl() ++ + pr_evar_map_constraints evm else pr_evar_map evm let explain_unsatisfiable_constraints env evd constr = - let evm = Evarutil.nf_evars evd in + let evm = Evarutil.nf_evar_map evd in let undef = Evd.undefined_evars evm in match constr with | None -> |