aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml27
-rw-r--r--plugins/ltac/extratactics.ml413
-rw-r--r--plugins/ltac/tactic_debug.ml14
-rw-r--r--plugins/quote/quote.ml2
-rw-r--r--plugins/setoid_ring/newring.ml20
5 files changed, 44 insertions, 32 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7c5efaea3a..1cb417bf47 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -397,33 +397,18 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
simplest_elim false_t]
end }
-let discriminate_tac (cstr,u as cstru) p =
+(* Essentially [assert (Heq : lhs = rhs) by proof_tac p; discriminate Heq] *)
+let discriminate_tac cstru p =
Proofview.Goal.enter { enter = begin fun gl ->
- let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
+ let lhs=constr_of_term p.p_lhs and rhs=constr_of_term p.p_rhs in
let env = Proofview.Goal.env gl in
- let concl = Proofview.Goal.concl gl in
- let xid = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
- let identity = Universes.constr_of_global (Lazy.force _I) in
- let identity = EConstr.of_constr identity in
- let trivial = Universes.constr_of_global (Lazy.force _True) in
- let trivial = EConstr.of_constr trivial in
let evm = Tacmach.New.project gl in
- let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in
- let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
- let outtype = mkSort outtype in
- let pred = mkLambda(Name xid,outtype,mkRel 1) in
+ let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl lhs) in
let hid = Tacmach.New.pf_get_new_id (Id.of_string "Heq") gl in
- let proj = build_projection intype cstru trivial concl gl in
- let injt = app_global _f_equal
- [|intype;outtype;proj;t1;t2;mkVar hid|] in
- let endt k =
- injt (fun injt ->
- app_global _eq_rect
- [|outtype;trivial;pred;identity;concl;injt|] k) in
- let neweq = app_global _eq [|intype;t1;t2|] in
+ let neweq=app_global _eq [|intype;lhs;rhs|] in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm)
(Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
- [proof_tac p; endt refine_exact_check])
+ [proof_tac p; Equality.discrHyp hid])
end }
(* wrap everything *)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 21419d1f92..3e6ccaf84a 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -812,6 +812,19 @@ TACTIC EXTEND destauto
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
+(**********************************************************************)
+
+(**********************************************************************)
+(* A version of abstract constructing transparent terms *)
+(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *)
+(**********************************************************************)
+
+TACTIC EXTEND transparent_abstract
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+ Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) } ]
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter { enter = fun gl ->
+ Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) } ]
+END
(* ********************************************************************* *)
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index dffeade298..dac15ff79e 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -85,6 +85,19 @@ let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0)
let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None)
+let batch = ref false
+
+open Goptions
+
+let _ =
+ declare_bool_option
+ { optsync = false;
+ optdepr = false;
+ optname = "Ltac batch debug";
+ optkey = ["Ltac";"Batch";"Debug"];
+ optread = (fun () -> !batch);
+ optwrite = (fun x -> batch := x) }
+
let rec drop_spaces inst i =
if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1)
else i
@@ -150,6 +163,7 @@ let rec prompt level =
begin
let open Proofview.NonLogical in
Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >>
+ if Pervasives.(!batch) then return (DebugOn (level+1)) else
let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in
Proofview.NonLogical.catch Proofview.NonLogical.read_line
begin function (e, info) -> match e with
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index fc9d70ae7d..c649cfb2c6 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -8,7 +8,7 @@
(* The `Quote' tactic *)
-(* The basic idea is to automatize the inversion of interpetation functions
+(* The basic idea is to automatize the inversion of interpretation functions
in 2-level approach
Examples are given in \texttt{theories/DEMOS/DemoQuote.v}
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index d59ffee546..6b8ef630a2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -333,12 +333,12 @@ let _ = add_map "ring"
my_reference "gen_phiZ", (function _->Eval);
(* Pphi_dev: evaluate polynomial and coef operations, protect
ring operations and make recursive call on the var map *)
- pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+ pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
pol_cst "Pphi_pow",
(function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
- (* PEeval: evaluate morphism and polynomial, protect ring
+ (* PEeval: evaluate polynomial, protect ring
operations and make recursive call on the var map *)
- pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
+ pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot)])
(****************************************************************************)
(* Ring database *)
@@ -780,20 +780,20 @@ let _ = add_map "field"
(* display_linear: evaluate polynomials and coef operations, protect
field operations and make recursive call on the var map *)
my_reference "display_linear",
- (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
+ (function -1|9|10|11|13|15|16->Eval|12|14->Rec|_->Prot);
my_reference "display_pow_linear",
(function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
(* Pphi_dev: evaluate polynomial and coef operations, protect
ring operations and make recursive call on the var map *)
- pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
+ pol_cst "Pphi_dev", (function -1|8|9|10|12|14->Eval|11|13->Rec|_->Prot);
pol_cst "Pphi_pow",
- (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
- (* PEeval: evaluate morphism and polynomial, protect ring
+ (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
+ (* PEeval: evaluate polynomial, protect ring
operations and make recursive call on the var map *)
- pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
- (* FEeval: evaluate morphism, protect field
+ pol_cst "PEeval", (function -1|10|13->Eval|8|12->Rec|_->Prot);
+ (* FEeval: evaluate polynomial, protect field
operations and make recursive call on the var map *)
- my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
+ my_reference "FEeval", (function -1|12|15->Eval|10|14->Rec|_->Prot)]);;
let _ = add_map "field_cond"
(map_without_eq
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 03:11:15 +0000