From 60520cd8d08f63337225c0a2938827e00a2c48a3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 10 Apr 2019 16:41:34 -0400 Subject: sed s'/RewriterProofs/RewriterAll/g' --- Makefile | 2 +- README.md | 10 ++-- _CoqProject | 4 +- src/BoundsPipeline.v | 6 +-- src/CompilersTestCases.v | 4 +- src/Rewriter/Arith.v | 6 +-- src/Rewriter/ArithWithCasts.v | 6 +-- src/Rewriter/NBE.v | 6 +-- src/Rewriter/StripLiteralCasts.v | 6 +-- src/Rewriter/ToFancy.v | 6 +-- src/Rewriter/ToFancyWithCasts.v | 6 +-- src/RewriterAll.v | 24 +++++++++ src/RewriterAllTactics.v | 107 +++++++++++++++++++++++++++++++++++++++ src/RewriterProofs.v | 24 --------- src/RewriterProofsTactics.v | 107 --------------------------------------- 15 files changed, 162 insertions(+), 162 deletions(-) create mode 100644 src/RewriterAll.v create mode 100644 src/RewriterAllTactics.v delete mode 100644 src/RewriterProofs.v delete mode 100644 src/RewriterProofsTactics.v diff --git a/Makefile b/Makefile index 42556fcf3..17d57cb07 100644 --- a/Makefile +++ b/Makefile @@ -51,7 +51,7 @@ LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \ src/RewriterWf1.vo \ src/RewriterWf2.vo \ src/RewriterRulesGood.vo \ - src/RewriterProofs.vo + src/RewriterAll.vo NOBIGMEM_UNMADE_VOFILES := \ src/Curves/Weierstrass/AffineProofs.vo \ src/Curves/Weierstrass/Jacobian.vo \ diff --git a/README.md b/README.md index 57ef3edf1..ae32333c5 100644 --- a/README.md +++ b/README.md @@ -204,7 +204,7 @@ Rewriter.v ←────────────────────── ↗ ↖ RewriterWf2.v RewriterInterpProofs1.v ↖ ↗ -RewriterRules.v RewriterProofsTactics.v +RewriterRules.v RewriterAllTactics.v ↑ ↑ RewriterRulesProofs.v │ ↑ │ @@ -218,7 +218,7 @@ RewriterRulesProofs.v │ ↑ ↑ │ └───────┬──────────────────┴───────────────────────────────────────────────────────┘ │ - RewriterProofs.v + RewriterAll.v ``` - RewriterRules.v: Defines the list of types of the rewrite rules that @@ -265,7 +265,7 @@ RewriterRulesProofs.v │ rewriter, taking in interp-goodness of rewrite rules as a hypothesis. -- RewriterProofsTactics.v: Defines the tactic +- RewriterAllTactics.v: Defines the tactic `RewriteRules.Tactic.make_rewriter` (and a similar tactic notation) which build the entire `VerifiedRewriter`. They take in the `include_interp` as in Rewriter.v tactics, as well as an hlist of @@ -274,12 +274,12 @@ RewriterRulesProofs.v │ rewriter from a list of rewrite rules. - Rewriter/{NBE, Arith, ArithWithCasts, StripLiteralCasts, ToFancy, - ToFancyWithCasts}.v: Use the tactic from RewriterProofsTactics.v + ToFancyWithCasts}.v: Use the tactic from RewriterAllTactics.v together with the proven list of rewrite rules from RewriterRulesProofs.v to reify and reduce the corresponding pass and generate a rewriter. -- RewriterProofs.v: `Definition`less file that `Export`s the rewriters +- RewriterAll.v: `Definition`less file that `Export`s the rewriters defined in `Rewriter/*.v` diff --git a/_CoqProject b/_CoqProject index 2ca7a4b89..4d4b652ff 100644 --- a/_CoqProject +++ b/_CoqProject @@ -36,8 +36,8 @@ src/MiscCompilerPassesProofs.v src/PreLanguage.v src/Rewriter.v src/RewriterInterpProofs1.v -src/RewriterProofs.v -src/RewriterProofsTactics.v +src/RewriterAll.v +src/RewriterAllTactics.v src/RewriterRules.v src/RewriterRulesProofs.v src/RewriterWf1.v diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index f0c161dc2..6c21d7c64 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -29,7 +29,7 @@ Require Crypto.CStringification. Require Crypto.LanguageWf. Require Crypto.UnderLetsProofs. Require Crypto.MiscCompilerPassesProofs. -Require Crypto.RewriterProofs. +Require Crypto.RewriterAll. Require Crypto.AbstractInterpretationWf. Require Crypto.AbstractInterpretationProofs. Require Import Crypto.Util.Notations. @@ -39,7 +39,7 @@ Import Crypto.LanguageWf Crypto.UnderLetsProofs Crypto.MiscCompilerPassesProofs - Crypto.RewriterProofs + Crypto.RewriterAll Crypto.AbstractInterpretationWf Crypto.AbstractInterpretationProofs Crypto.Language @@ -53,7 +53,7 @@ Import LanguageWf.Compilers UnderLetsProofs.Compilers MiscCompilerPassesProofs.Compilers - RewriterProofs.Compilers + RewriterAll.Compilers AbstractInterpretationWf.Compilers AbstractInterpretationProofs.Compilers Language.Compilers diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v index 2ed149cdd..91fc3af1d 100644 --- a/src/CompilersTestCases.v +++ b/src/CompilersTestCases.v @@ -5,7 +5,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Language. Require Import Crypto.UnderLets. Require Import Crypto.AbstractInterpretation. -Require Import Crypto.RewriterProofs. +Require Import Crypto.RewriterAll. Require Import Crypto.MiscCompilerPasses. Require Import Crypto.CStringification. Import ListNotations. Local Open Scope Z_scope. @@ -13,7 +13,7 @@ Import ListNotations. Local Open Scope Z_scope. Import Language.Compilers. Import UnderLets.Compilers. Import AbstractInterpretation.Compilers. -Import RewriterProofs.Compilers. +Import RewriterAll.Compilers. Import MiscCompilerPasses.Compilers. Import CStringification.Compilers. Local Coercion Z.of_nat : nat >-> Z. diff --git a/src/Rewriter/Arith.v b/src/Rewriter/Arith.v index cae1526d2..7b368cb16 100644 --- a/src/Rewriter/Arith.v +++ b/src/Rewriter/Arith.v @@ -1,15 +1,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ArithWithCasts.v b/src/Rewriter/ArithWithCasts.v index de17f207e..554457f1d 100644 --- a/src/Rewriter/ArithWithCasts.v +++ b/src/Rewriter/ArithWithCasts.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/NBE.v b/src/Rewriter/NBE.v index 64e38a38d..db0670179 100644 --- a/src/Rewriter/NBE.v +++ b/src/Rewriter/NBE.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/StripLiteralCasts.v b/src/Rewriter/StripLiteralCasts.v index 0f35dfed6..8c6c1799c 100644 --- a/src/Rewriter/StripLiteralCasts.v +++ b/src/Rewriter/StripLiteralCasts.v @@ -1,14 +1,14 @@ Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ToFancy.v b/src/Rewriter/ToFancy.v index da18848ba..da77e4f21 100644 --- a/src/Rewriter/ToFancy.v +++ b/src/Rewriter/ToFancy.v @@ -1,15 +1,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/Rewriter/ToFancyWithCasts.v b/src/Rewriter/ToFancyWithCasts.v index 714ea071e..b8e268b1c 100644 --- a/src/Rewriter/ToFancyWithCasts.v +++ b/src/Rewriter/ToFancyWithCasts.v @@ -2,15 +2,15 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.Language. Require Import Crypto.LanguageWf. Require Import Crypto.Util.ZRange. -Require Import Crypto.RewriterProofsTactics. +Require Import Crypto.RewriterAllTactics. Require Import Crypto.RewriterRulesProofs. Module Compilers. Import Language.Compilers. Import Language.Compilers.defaults. Import LanguageWf.Compilers. - Import RewriterProofsTactics.Compilers.RewriteRules.GoalType. - Import RewriterProofsTactics.Compilers.RewriteRules.Tactic. + Import RewriterAllTactics.Compilers.RewriteRules.GoalType. + Import RewriterAllTactics.Compilers.RewriteRules.Tactic. Module Import RewriteRules. Section __. diff --git a/src/RewriterAll.v b/src/RewriterAll.v new file mode 100644 index 000000000..c2a891de1 --- /dev/null +++ b/src/RewriterAll.v @@ -0,0 +1,24 @@ +Require Import Crypto.Rewriter.NBE. +Require Import Crypto.Rewriter.Arith. +Require Import Crypto.Rewriter.ArithWithCasts. +Require Import Crypto.Rewriter.StripLiteralCasts. +Require Import Crypto.Rewriter.ToFancy. +Require Import Crypto.Rewriter.ToFancyWithCasts. + +Module Compilers. + Export NBE.Compilers. + Export Arith.Compilers. + Export ArithWithCasts.Compilers. + Export StripLiteralCasts.Compilers. + Export ToFancy.Compilers. + Export ToFancyWithCasts.Compilers. + + Module Import RewriteRules. + Export NBE.Compilers.RewriteRules. + Export Arith.Compilers.RewriteRules. + Export ArithWithCasts.Compilers.RewriteRules. + Export StripLiteralCasts.Compilers.RewriteRules. + Export ToFancy.Compilers.RewriteRules. + Export ToFancyWithCasts.Compilers.RewriteRules. + End RewriteRules. +End Compilers. diff --git a/src/RewriterAllTactics.v b/src/RewriterAllTactics.v new file mode 100644 index 000000000..22fd16cbb --- /dev/null +++ b/src/RewriterAllTactics.v @@ -0,0 +1,107 @@ +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. +Require Import Crypto.RewriterWf2. +Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Util.Tactics.ConstrFail. + +Module Compilers. + Import LanguageWf.Compilers. + Import GENERATEDIdentifiersWithoutTypes.Compilers. + Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. + Import Rewriter.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules. + Import RewriterWf2.Compilers.RewriteRules. + Import RewriterInterpProofs1.Compilers.RewriteRules. + Import Rewriter.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. + + Module Import RewriteRules. + Definition VerifiedRewriter_of_Rewriter + (R : RewriterT) + (RWf : Wf_GoalT R) + (RInterp : Interp_GoalT R) + (RProofs : PrimitiveHList.hlist + (@snd bool Prop) + (List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R)))) + : VerifiedRewriter. + Proof. + simple refine + (let HWf := _ in + let HInterp_gen := _ in + @Build_VerifiedRewriter (@Rewriter.Compilers.RewriteRules.GoalType.Rewrite R) HWf HInterp_gen (HInterp_gen _)); + [ | clear HWf ]; intros. + all: abstract ( + rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq; + first [ apply Compile.Wf_Rewrite; [ | assumption ]; + let wf_do_again := fresh "wf_do_again" in + (intros ? ? ? ? wf_do_again ? ?); + eapply @Compile.wf_assemble_identifier_rewriters; + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct + with nocore; + try reflexivity + | eapply Compile.InterpRewrite; [ | assumption ]; + intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, + @ident.gen_interp_Proper, eq_refl + with nocore ]). + Defined. + + Ltac make_VerifiedRewriter R RWf RInterp RProofs := + let res := (eval hnf in (@VerifiedRewriter_of_Rewriter R RWf RInterp RProofs)) in + let res := lazymatch res with + | context Res[@Build_VerifiedRewriter ?R] + => let t := fresh "t" in + let R' := fresh in + let R' := constr:(fun t + => match R t return _ with + | R' => ltac:(let v := (eval hnf in R') in exact v) + end) in + context Res[@Build_VerifiedRewriter R'] + end in + res. + + Ltac Build_Rewriter include_interp specs_proofs := + let specs := lazymatch type of specs_proofs with + | PrimitiveHList.hlist (@snd bool Prop) ?specs => specs + | ?T + => let expected_type := uconstr:(PrimitiveHList.hlist (@snd bool Prop) ?[specs]) in + constr_fail_with ltac:(fun _ => fail 1 "Invalid type for specs_proofs:" T "Expected:" expected_type) + end in + let R_name := fresh "Rewriter_data" in + let R := Build_RewriterT include_interp specs in + let R := cache_term R R_name in + let Rwf := fresh "Rewriter_Wf" in + let Rwf := cache_proof_with_type_by (Wf_GoalT R) ltac:(idtac; prove_good ()) Rwf in + let RInterp := fresh "Rewriter_Interp" in + let RInterp := cache_proof_with_type_by (Interp_GoalT R) ltac:(idtac; prove_interp_good ()) RInterp in + make_VerifiedRewriter R Rwf RInterp specs_proofs. + + Module Export GoalType. + Export RewriterWf1.Compilers.RewriteRules.GoalType. + End GoalType. + + Module Export Tactic. + Module Export Settings. + Export Rewriter.Compilers.RewriteRules.Tactic.Settings. + End Settings. + + Ltac make_rewriter include_interp specs_proofs := + let res := Build_Rewriter include_interp specs_proofs in refine res. + + Tactic Notation "make_rewriter" constr(include_interp) constr(specs_proofs) := + make_rewriter include_interp specs_proofs. + End Tactic. + End RewriteRules. +End Compilers. diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v deleted file mode 100644 index c2a891de1..000000000 --- a/src/RewriterProofs.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Crypto.Rewriter.NBE. -Require Import Crypto.Rewriter.Arith. -Require Import Crypto.Rewriter.ArithWithCasts. -Require Import Crypto.Rewriter.StripLiteralCasts. -Require Import Crypto.Rewriter.ToFancy. -Require Import Crypto.Rewriter.ToFancyWithCasts. - -Module Compilers. - Export NBE.Compilers. - Export Arith.Compilers. - Export ArithWithCasts.Compilers. - Export StripLiteralCasts.Compilers. - Export ToFancy.Compilers. - Export ToFancyWithCasts.Compilers. - - Module Import RewriteRules. - Export NBE.Compilers.RewriteRules. - Export Arith.Compilers.RewriteRules. - Export ArithWithCasts.Compilers.RewriteRules. - Export StripLiteralCasts.Compilers.RewriteRules. - Export ToFancy.Compilers.RewriteRules. - Export ToFancyWithCasts.Compilers.RewriteRules. - End RewriteRules. -End Compilers. diff --git a/src/RewriterProofsTactics.v b/src/RewriterProofsTactics.v deleted file mode 100644 index 22fd16cbb..000000000 --- a/src/RewriterProofsTactics.v +++ /dev/null @@ -1,107 +0,0 @@ -Require Import Crypto.Language. -Require Import Crypto.LanguageInversion. -Require Import Crypto.LanguageWf. -Require Import Crypto.UnderLetsProofs. -Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. -Require Import Crypto.Rewriter. -Require Import Crypto.RewriterWf1. -Require Import Crypto.RewriterWf2. -Require Import Crypto.RewriterInterpProofs1. -Require Import Crypto.Util.Tactics.CacheTerm. -Require Import Crypto.Util.Tactics.ConstrFail. - -Module Compilers. - Import LanguageWf.Compilers. - Import GENERATEDIdentifiersWithoutTypes.Compilers. - Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. - Import Rewriter.Compilers.RewriteRules. - Import RewriterWf1.Compilers.RewriteRules. - Import RewriterWf2.Compilers.RewriteRules. - Import RewriterInterpProofs1.Compilers.RewriteRules. - Import Rewriter.Compilers.RewriteRules.GoalType. - Import RewriterWf1.Compilers.RewriteRules.GoalType. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. - Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. - Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. - - Module Import RewriteRules. - Definition VerifiedRewriter_of_Rewriter - (R : RewriterT) - (RWf : Wf_GoalT R) - (RInterp : Interp_GoalT R) - (RProofs : PrimitiveHList.hlist - (@snd bool Prop) - (List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R)))) - : VerifiedRewriter. - Proof. - simple refine - (let HWf := _ in - let HInterp_gen := _ in - @Build_VerifiedRewriter (@Rewriter.Compilers.RewriteRules.GoalType.Rewrite R) HWf HInterp_gen (HInterp_gen _)); - [ | clear HWf ]; intros. - all: abstract ( - rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq; - first [ apply Compile.Wf_Rewrite; [ | assumption ]; - let wf_do_again := fresh "wf_do_again" in - (intros ? ? ? ? wf_do_again ? ?); - eapply @Compile.wf_assemble_identifier_rewriters; - eauto using - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct - with nocore; - try reflexivity - | eapply Compile.InterpRewrite; [ | assumption ]; - intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); - eauto using - pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, - @ident.gen_interp_Proper, eq_refl - with nocore ]). - Defined. - - Ltac make_VerifiedRewriter R RWf RInterp RProofs := - let res := (eval hnf in (@VerifiedRewriter_of_Rewriter R RWf RInterp RProofs)) in - let res := lazymatch res with - | context Res[@Build_VerifiedRewriter ?R] - => let t := fresh "t" in - let R' := fresh in - let R' := constr:(fun t - => match R t return _ with - | R' => ltac:(let v := (eval hnf in R') in exact v) - end) in - context Res[@Build_VerifiedRewriter R'] - end in - res. - - Ltac Build_Rewriter include_interp specs_proofs := - let specs := lazymatch type of specs_proofs with - | PrimitiveHList.hlist (@snd bool Prop) ?specs => specs - | ?T - => let expected_type := uconstr:(PrimitiveHList.hlist (@snd bool Prop) ?[specs]) in - constr_fail_with ltac:(fun _ => fail 1 "Invalid type for specs_proofs:" T "Expected:" expected_type) - end in - let R_name := fresh "Rewriter_data" in - let R := Build_RewriterT include_interp specs in - let R := cache_term R R_name in - let Rwf := fresh "Rewriter_Wf" in - let Rwf := cache_proof_with_type_by (Wf_GoalT R) ltac:(idtac; prove_good ()) Rwf in - let RInterp := fresh "Rewriter_Interp" in - let RInterp := cache_proof_with_type_by (Interp_GoalT R) ltac:(idtac; prove_interp_good ()) RInterp in - make_VerifiedRewriter R Rwf RInterp specs_proofs. - - Module Export GoalType. - Export RewriterWf1.Compilers.RewriteRules.GoalType. - End GoalType. - - Module Export Tactic. - Module Export Settings. - Export Rewriter.Compilers.RewriteRules.Tactic.Settings. - End Settings. - - Ltac make_rewriter include_interp specs_proofs := - let res := Build_Rewriter include_interp specs_proofs in refine res. - - Tactic Notation "make_rewriter" constr(include_interp) constr(specs_proofs) := - make_rewriter include_interp specs_proofs. - End Tactic. - End RewriteRules. -End Compilers. -- cgit v1.2.3