diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 3 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 15 |
2 files changed, 9 insertions, 9 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index aa71a45658..5dea4631c4 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -29,8 +29,7 @@ let debug x = let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 1cb417bf47..43c06a54d4 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -26,7 +26,7 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) +let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) let _f_equal = reference ["Init";"Logic"] "f_equal" let _eq_rect = reference ["Init";"Logic"] "eq_rect" @@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms = let build_projection intype (cstr:pconstructor) special default gls= let open Tacmach.New in let ci= (snd(fst cstr)) in - let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in + let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in let id=pf_get_new_id (Id.of_string "t") gls in - mkLambda(Name id,intype,body) + sigma, mkLambda(Name id,intype,body) (* generate an adhoc tactic following the proof tree *) @@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic = let special=mkRel (1+nargs-argind) in refresh_universes (type_of ti) (fun intype -> refresh_universes (type_of default) (fun outtype -> - let proj = + let sigma, proj = build_projection intype cstr special default gl in let injt= app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in - Tacticals.New.tclTHEN injt (proof_tac prf))) + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tacticals.New.tclTHEN injt (proof_tac prf)))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end } @@ -442,11 +443,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."); |