diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 11:16:35 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 11:16:35 +0200 |
| commit | f2fec63025d933f56dabf114a51720b1aae626c1 (patch) | |
| tree | 7f729302601fef48e6c59534a7904c7dfb92df2d /plugins/cc | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
| parent | 94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff) | |
Merge PR#402: Uniform attribute handling in interfaces
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 1cb417bf4..201726d1e 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -442,11 +442,11 @@ 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 = GHole (Loc.ghost, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = CAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype ~lax:true false [] env sigma c in let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env (GApp (Loc.ghost, c, holes)) + Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes)) in Feedback.msg_info (Pp.str "Goal is solvable by congruence but some arguments are missing."); |