diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index d19817e7..2eaa6146 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -49,7 +49,7 @@ let whd_delta env sigma t = (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = snd (sort_of env sigma c) let rec decompose_term env sigma t= match EConstr.kind sigma (whd env sigma t) with @@ -84,13 +84,13 @@ let rec decompose_term env sigma t= let canon_const = Constant.make1 (Constant.canonical c) in (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> - let canon_const kn = Constant.make1 (Constant.canonical kn) in - let p' = Projection.map canon_const p in + let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in + let p' = Projection.map canon_mind p in let c = Retyping.expand_projection env sigma p' c [] in decompose_term env sigma c | _ -> let t = Termops.strip_outer_cast sigma t in - if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found + if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found (* decompose equality in members and type *) open Termops @@ -264,9 +264,8 @@ let app_global_with_holes f args n = let ans = mkApp (fc, args) in let (sigma, holes) = gen_holes env sigma t n [] in let ans = applist (ans, holes) in - let evdref = ref sigma in - let () = Typing.e_check env evdref ans concl in - (!evdref, ans) + let sigma = Typing.check env sigma ans concl in + (sigma, ans) end end @@ -444,7 +443,7 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in |