diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 13 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 14 | ||||
| -rw-r--r-- | plugins/quote/quote.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 20 |
4 files changed, 38 insertions, 11 deletions
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 |