diff options
| -rw-r--r-- | pretyping/evarutil.ml | 26 | ||||
| -rw-r--r-- | pretyping/termops.ml | 7 | ||||
| -rw-r--r-- | pretyping/termops.mli | 1 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 10 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 26 |
6 files changed, 49 insertions, 23 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 549160715..aed50c468 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -891,6 +891,12 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) +and occur_existential evm c = + let rec occrec c = match kind_of_term c with + | Evar (e, _) -> if not (is_defined evm e) then raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + and evar_define env (evk,_ as ev) rhs evd = try let (evd',body) = invert_definition env evd ev rhs in @@ -1045,12 +1051,22 @@ let solve_simple_eqn conv_algo env evd (pbty,(evk1,args1 as ev1),t2) = then solve_evar_evar evar_define env evd ev1 ev2 else add_conv_pb (pbty,env,mkEvar ev1,t2) evd | _ -> - evar_define env ev1 t2 evd in + let evd = evar_define env ev1 t2 evd in + let evm = evars_of evd in + let evi = Evd.find evm evk1 in + if occur_existential evm evi.evar_concl then + let evenv = evar_env evi in + let evc = nf_isevar evd evi.evar_concl in + let body = match evi.evar_body with Evar_defined b -> b | Evar_empty -> assert false in + let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in + fst (conv_algo evenv evd Reduction.CUMUL ty evc) + else evd + in let (evd,pbs) = extract_changed_conv_pbs evd status_changed in - List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then conv_algo env evd pbty t1 t2 else p) (evd,true) - pbs + List.fold_left + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then conv_algo env evd pbty t1 t2 else p) (evd,true) + pbs with e when precatchable_exception e -> (evd,false) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index aa6cc297b..99252ce65 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -473,6 +473,13 @@ let occur_existential c = | _ -> iter_constr occrec c in try occrec c; false with Occur -> true +let occur_meta_or_existential c = + let rec occrec c = match kind_of_term c with + | Evar _ -> raise Occur + | Meta _ -> raise Occur + | _ -> iter_constr occrec c + in try occrec c; false with Occur -> true + let occur_const s c = let rec occur_rec c = match kind_of_term c with | Const sp when sp=s -> raise Occur diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 92c0a78d4..f5f1a459f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -93,6 +93,7 @@ val strip_head_cast : constr -> constr exception Occur val occur_meta : types -> bool val occur_existential : types -> bool +val occur_meta_or_existential : types -> bool val occur_const : constant -> types -> bool val occur_evar : existential_key -> types -> bool val occur_in_global : env -> identifier -> constr -> unit diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c437d9eab..1f1bdb4ff 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -30,7 +30,7 @@ type typeclass = { (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itselft. *) + gives a direct link to the class itself. *) cl_context : (global_reference * bool) option list * rel_context; (* Context of definitions and properties on defs, will not be shared *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a2671b5d1..9444d9137 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -521,12 +521,8 @@ let w_merge env with_types flags (metas,evars) evd = let evd' = mimick_evar evd flags f (Array.length cl) evn in w_merge_rec evd' metas evars eqns | _ -> - let evi = Evd.find (evars_of evd) evn in - let env' = push_rels_assum (List.map (fun (_,t) -> Anonymous,t) evars') env in - let rty = Retyping.get_type_of_with_meta env' (evars_of evd) (metas_of evd) rhs' in - let evd', rhs'' = w_coerce_to_type env' evd rhs' rty evi.evar_concl in - let evd'' = solve_simple_evar_eqn env' evd' ev rhs'' in - w_merge_rec evd'' metas evars' eqns + w_merge_rec (solve_simple_evar_eqn env evd ev rhs') + metas evars' eqns end | [] -> @@ -694,7 +690,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd = if isMeta op then if allow_K then (evd,op::l) else error "Match_subterm" - else if occur_meta op then + else if occur_meta_or_existential op then let (evd',cl) = try (* This is up to delta for subterms w/o metas ... *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f253a0a7a..f760e731b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -316,7 +316,13 @@ let explain_occur_check env ev rhs = str "Cannot define " ++ str id ++ str " with term" ++ brk(1,1) ++ pt ++ spc () ++ str "that would depend on itself." -let explain_hole_kind env = function +let pr_ne_context_of header footer env = + if Environ.rel_context env = empty_rel_context & + Environ.named_context env = empty_named_context + then footer + else pr_ne_context_of header env + +let explain_hole_kind env evi = function | QuestionMark _ -> str "this placeholder" | CasesType -> str "the type of this pattern-matching problem" @@ -330,7 +336,12 @@ let explain_hole_kind env = function pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c | InternalHole -> - str "an internal placeholder" + str "an internal placeholder" ++ + Option.cata (fun evi -> + let env = Evd.evar_env evi in + str " of type " ++ pr_lconstr_env env evi.evar_concl ++ + pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env) + (mt ()) evi | TomatchTypeParameter (tyi,n) -> str "the " ++ nth n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ @@ -344,7 +355,7 @@ let explain_not_clean env ev t k = let env = make_all_name_different env in let id = Evd.string_of_existential ev in let var = pr_lconstr_env env t in - str "Tried to instantiate " ++ explain_hole_kind env k ++ + str "Tried to instantiate " ++ explain_hole_kind env None k ++ str " (" ++ str id ++ str ")" ++ spc () ++ str "with a term using variable " ++ var ++ spc () ++ str "which is not in its scope." @@ -354,14 +365,9 @@ let explain_unsolvability = function | Some (SeveralInstancesFound n) -> strbrk " (several distinct possible instances found)" -let pr_ne_context_of header footer env = - if Environ.rel_context env = empty_rel_context & - Environ.named_context env = empty_named_context then footer - else pr_ne_context_of header env - let explain_typeclass_resolution env evi k = match k with - | InternalHole | ImplicitArg _ -> + | GoalEvar | InternalHole | ImplicitArg _ -> (match Typeclasses.class_of_constr evi.evar_concl with | Some c -> let env = Evd.evar_env evi in @@ -372,7 +378,7 @@ let explain_typeclass_resolution env evi k = | _ -> mt() let explain_unsolvable_implicit env evi k explain = - str "Cannot infer " ++ explain_hole_kind env k ++ + str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++ explain_unsolvability explain ++ str "." ++ explain_typeclass_resolution env evi k |