diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-21 15:49:30 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-21 15:49:30 +0000 |
| commit | 70aa6184a399ebf2b70bf284ad57fc4e4dd5c226 (patch) | |
| tree | ffc803cda254ce791f81e48b763b4d5e84dfe990 /toplevel | |
| parent | 994048e670339c3709f7735446b40341d21aa6a9 (diff) | |
Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside
inductive and Program defs. Fix eterm bug when generating obligations
and remove optimization of let-in removal which prevents factorization
of proofs/"asserts" in Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11330 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 1 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 12 |
2 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 413146ca7..f18cecb20 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -539,6 +539,7 @@ let interp_mutual paramsl indl notations finite = (* Instantiate evars and check all are resolved *) let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in let sigma = evars_of evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 422555d04..ea2d53ff2 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -504,7 +504,7 @@ let explain_no_instance env (_,id) l = str "applied to arguments" ++ spc () ++ prlist_with_sep pr_spc (pr_lconstr_env env) l -let pr_constraints env evm = +let pr_constraints printenv env evm = let l = Evd.to_list evm in let (ev, evi) = List.hd l in if List.for_all (fun (ev', evi') -> @@ -512,7 +512,7 @@ let pr_constraints env evm = then let pe = pr_ne_context_of (str "In environment:") (mt ()) (reset_with_named_context evi.evar_hyps env) in - pe ++ fnl () ++ + (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 else @@ -522,13 +522,13 @@ let explain_unsatisfiable_constraints env evd constr = let evm = Evd.evars_of evd in match constr with | None -> - str"Unable to satisfy the following typeclass constraints:" ++ fnl() ++ - pr_constraints env evm + str"Unable to satisfy the following constraints:" ++ fnl() ++ + pr_constraints true env evm | Some (evi, k) -> explain_unsolvable_implicit env evi k None ++ fnl () ++ if List.length (Evd.to_list evm) > 1 then - str"With the following meta variables:" ++ - fnl() ++ Evd.pr_evar_map evm + str"With the following constraints:" ++ fnl() ++ + pr_constraints false env evm else mt () let explain_mismatched_contexts env c i j = |