diff options
Diffstat (limited to 'rewrite.ml4')
| -rw-r--r-- | rewrite.ml4 | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/rewrite.ml4 b/rewrite.ml4 index b3e52e0..1f57c0b 100644 --- a/rewrite.ml4 +++ b/rewrite.ml4 @@ -8,6 +8,11 @@ (** aac_rewrite -- rewriting modulo *) +open Pcoq.Prim +open Pcoq.Constr +open Stdarg +open Constrarg + DECLARE PLUGIN "aac" module Control = struct @@ -33,7 +38,7 @@ let retype = Coq.retype (* helper to be used with the previous function: raise a new anomaly except if a another one was previously raised *) let push_anomaly msg = function - | e when Errors.is_anomaly e -> raise e + | e when CErrors.is_anomaly e -> raise e | _ -> Coq.anomaly msg module M = Matcher @@ -190,7 +195,7 @@ let by_aac_reflexivity zero [ retype decision_thm; retype convert_to; convert ; tac_or_exn apply_tac Coq.user_error "unification failure"; - tac_or_exn (time_tac "vm_norm" (Tactics.normalise_in_concl)) Coq.anomaly "vm_compute failure"; + tac_or_exn (time_tac "vm_norm" (Proofview.V82.of_tactic (Tactics.normalise_in_concl))) Coq.anomaly "vm_compute failure"; Tacticals.tclORELSE (Proofview.V82.of_tactic Tactics.reflexivity) (Tacticals.tclFAIL 0 (Pp.str "Not an equality modulo A/AC")) ]) @@ -253,25 +258,19 @@ let aac_conclude | Not_found -> Coq.user_error "No lifting from the goal's relation to an equivalence" open Libnames +open Tacexpr open Tacinterp let aac_normalise = fun goal -> let ids = Tacmach.pf_ids_of_hyps goal in + let loc = Loc.ghost in + let mp = MPfile (DirPath.make (List.map Id.of_string ["AAC"; "AAC_tactics"])) in + let norm_tac = KerName.make2 mp (Label.make "internal_normalize") in + let norm_tac = Misctypes.ArgArg (loc, norm_tac) in Tacticals.tclTHENLIST [ aac_conclude by_aac_normalise; - Proofview.V82.of_tactic begin - Tacinterp.interp ( - <:tactic< - intro x; - intro y; - vm_compute in x; - vm_compute in y; - unfold x; - unfold y; - compute [Internal.eval Internal.fold_map Internal.copy Prect]; simpl - >> - )end; + Proofview.V82.of_tactic (Tacinterp.eval_tactic (TacArg (loc, TacCall (loc, norm_tac, [])))); Proofview.V82.of_tactic (Tactics.keep ids) ] goal |