diff options
| -rw-r--r-- | contrib/subtac/eterm.ml | 6 | ||||
| -rw-r--r-- | contrib/subtac/eterm.mli | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 2 | ||||
| -rw-r--r-- | toplevel/command.ml | 1 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 12 |
6 files changed, 13 insertions, 14 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 9bfb33ea7..c2309c833 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -46,7 +46,7 @@ let subst_evar_constr evs n t = let rec aux hyps args acc = match hyps, args with ((_, None, _) :: tlh), (c :: tla) -> - aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc) + aux tlh tla ((substrec (depth, fixrels) c) :: acc) | ((_, Some _, _) :: tlh), (_ :: tla) -> aux tlh tla acc | [], [] -> acc @@ -93,8 +93,8 @@ let etype_of_evar evs hyps concl = let trans' = Idset.union trans trans' in (match copt with Some c -> - if noccurn 1 rest then lift (-1) rest, s', trans' - else +(* if noccurn 1 rest then lift (-1) rest, s', trans' *) +(* else *) let c', s'', trans'' = subst_evar_constr evs n c in let c' = subst_vars acc 0 c' in mkNamedProd_or_LetIn (id, Some c', t'') rest, diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index 5f10ac1d3..bf854abb3 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -16,8 +16,6 @@ open Util val mkMetas : int -> constr list -(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) - (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index a393e2c9b..130d6858b 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -562,8 +562,8 @@ let next_obligation n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in let i = - array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) - obls + try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls + with Not_found -> anomaly "Could not find a solvable obligation." in solve_obligation prg i let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index 78ee2f5ce..f65e3f786 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -73,7 +73,7 @@ let interp env isevars c tycon = let _ = isevars := Evarutil.nf_evar_defs !isevars in let evd,_ = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) - let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in + let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in let evm = evars_of unevd' in isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type 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 = |