diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/README | 2 | ||||
| -rw-r--r-- | plugins/cc/ccproof.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 43 |
3 files changed, 21 insertions, 26 deletions
diff --git a/plugins/cc/README b/plugins/cc/README index c616b5daab..7df7b971e8 100644 --- a/plugins/cc/README +++ b/plugins/cc/README @@ -9,7 +9,7 @@ Files : - ccalgo.ml : congruence closure algorithm - ccproof.ml : proof generation code -- cctac.ml4 : the tactic itself +- cctac.mlg : the tactic itself - CCSolve.v : a small Ltac tactic based on congruence Known Bugs : the congruence tactic can fail due to type dependencies. diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index ef012e5092..f47a14cdc7 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file uses the (non-compressed) union-find structure to generate *) -(* proof-trees that will be transformed into proof-terms in cctac.ml4 *) +(* proof-trees that will be transformed into proof-terms in cctac.mlg *) open CErrors open Constr diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 3ed843649e..b5be1cdd89 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -437,30 +437,25 @@ let cc_tactic depth additionnal_terms = let cstr=(get_constructor_info uf ipac.cnode).ci_constr in discriminate_tac cstr p | Incomplete -> - 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, 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 - Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) - in - Feedback.msg_info - (Pp.str "Goal is solvable by congruence but some arguments are missing."); - Feedback.msg_info - (Pp.str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ - prlist_with_sep - (fun () -> str ")" ++ spc () ++ str "(") - pr_missing - terms_to_complete ++ - str ")\"," - end ++ - Pp.str " replacing metavariables by arbitrary terms."); - Tacticals.New.tclFAIL 0 (str "Incomplete") + 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, 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 + Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) + in + let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." + ++ fnl () ++ + str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") + pr_missing terms_to_complete ++ str ")\"," + end ++ + str " replacing metavariables by arbitrary terms.") in + Tacticals.New.tclFAIL 0 msg | Contradiction dis -> let env = Proofview.Goal.env gl in let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in |