diff options
Diffstat (limited to 'plugins/ssr/ssrview.ml')
| -rw-r--r-- | plugins/ssr/ssrview.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index aa614fbc1..faebe3179 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p = let mkGHole = DAst.make - (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)) + (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)) let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else [] let mkGApp f args = if args = [] then f @@ -254,18 +254,18 @@ let finalize_view s0 ?(simple_types=true) p = Goal.enter_one ~__LOC__ begin fun g -> let env = Goal.env g in let sigma = Goal.sigma g in - let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in + let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let filter x _ = Evar.Set.mem x evars_of_p in let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in let p = Reductionops.nf_evar sigma p in let get_body = function Evd.Evar_defined x -> x | _ -> assert false in let evars_of_econstr sigma t = - Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in + Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in let rigid_of s = List.fold_left (fun l k -> if Evd.is_defined sigma k then let bo = get_body Evd.(evar_body (find sigma k)) in - k :: l @ Evar.Set.elements (evars_of_econstr sigma bo) + k :: l @ Evar.Set.elements (evars_of_econstr sigma (EConstr.Unsafe.to_constr bo)) else l ) [] s in let und0 = (* Unassigned evars in the initial goal *) |