diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 18 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 1 | ||||
| -rw-r--r-- | plugins/ltac/g_class.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 35 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 16 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 63 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 5 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 1 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 183 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 14 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 75 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 7 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 5 | ||||
| -rw-r--r-- | plugins/ltac/tauto.ml | 18 |
16 files changed, 243 insertions, 208 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 0428f08138..f5098d2a34 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac @@ -348,6 +349,7 @@ let constr_flags () = { Pretyping.fail_evar = false; Pretyping.expand_evars = true; Pretyping.program_mode = false; + Pretyping.polymorphic = false; } let refine_tac ist simple with_classes c = @@ -813,9 +815,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; } END (* ********************************************************************* *) @@ -913,9 +915,9 @@ END the semantics of the LCF-style tactics, hence with the classic tactic mode. *) VERNAC COMMAND EXTEND GrabEvars -| [ "Grab" "Existential" "Variables" ] +| ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } END (* Shelves all the goals under focus. *) @@ -945,9 +947,9 @@ END (* Command to add every unshelved variables to the focus *) VERNAC COMMAND EXTEND Unshelve -| [ "Unshelve" ] +| ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } + -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1098,8 +1100,8 @@ END VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { Proof_global.compact_the_proof () } +| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> + { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 3a4b0571d4..523c7c8305 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -58,6 +58,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } in let map c env sigma = c env sigma in List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 3f2fabeeee..049a699cbd 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -84,7 +84,7 @@ TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> { typeclasses_eauto ~depth:d l } | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { - typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] } + typeclasses_eauto ~only_classes:true ~depth:d [Class_tactics.typeclasses_db] } END TACTIC EXTEND head_of_constr diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index a348e2cea4..7eb34158e8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -374,20 +374,21 @@ let () = declare_int_option { optwrite = fun n -> print_info_trace := n; } -let vernac_solve n info tcom b = +let vernac_solve ~pstate n info tcom b = let open Goal_select in - let status = Proof_global.with_current_proof (fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info !print_info_trace in - let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) in - if not status then Feedback.feedback Feedback.AddedAxiom + let pstate, status = Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let global = match n with SelectAll | SelectList _ -> true | _ -> false in + let info = Option.append info !print_info_trace in + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) pstate in + if not status then Feedback.feedback Feedback.AddedAxiom; + Some pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -434,12 +435,12 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } VERNAC { tactic_mode } EXTEND VernacSolve -| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def + Vernacentries.vernac_require_open_proof vernac_solve g n t def } -| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in @@ -449,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve VtLater } -> { let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def + Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index a12dee48a8..de3a9c9fa9 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac +let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) +let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| [ "Obligation" integer(num) withtac(tac) ] -> +| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 86a227415a..469551809c 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,64 +234,64 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts [] a aeq t n; + add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid atts binders a aeq t n; + add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { VtUnknown, VtNow } -> { - add_morphism_infer atts m n; + add_morphism_infer atts m n } - | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts [] m s n; + add_morphism atts [] m s n } - | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { - add_morphism atts binders m s n; + add_morphism atts binders m s n } END @@ -310,7 +310,12 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } +| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { (* This command should not use the proof env, keeping previous + behavior as requested in review. *) + fun ~pstate -> + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); + pstate } END diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 7bf705ffeb..a2dd51643b 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq = match stream_nth 0 strm with | KEYWORD "(" -> (match stream_nth 1 strm with - | IDENT _ | INT _ -> + | IDENT _ | NUMERAL _ -> (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) @@ -147,7 +147,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with end | _ -> ElimOnConstr clbind -let mkNumeral n = Numeral (string_of_int (abs n), 0<=n) +let mkNumeral n = + Numeral ((if 0<=n then SPlus else SMinus),NumTok.int (string_of_int (abs n))) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 1bdba699f7..80070a7493 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) - let pr_glob_constr_pptac env sigma c = pr_glob_constr_env env c diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b1d5c0252f..2d40ba6562 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -119,7 +119,7 @@ let app_poly_check env evars f args = (evars, cstrs), t let app_poly_nocheck env evars f args = - let evars, fc = f evars in + let evars, fc = f evars in evars, mkApp (fc, args) let app_poly_sort b = @@ -175,25 +175,29 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (find_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) - - let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) - - let proper_type = - let l = lazy (Lazy.force proper_class).cl_impl in - fun (evd,cstrs) -> - let (evd, c) = Evarutil.new_global evd (Lazy.force l) in - (evd, cstrs), c - - let proper_proxy_type = - let l = lazy (Lazy.force proper_proxy_class).cl_impl in - fun (evd,cstrs) -> - let (evd, c) = Evarutil.new_global evd (Lazy.force l) in - (evd, cstrs), c + let proper_class = + let r = lazy (find_reference morphisms "Proper") in + fun env sigma -> class_info env sigma (Lazy.force r) + + let proper_proxy_class = + let r = lazy (find_reference morphisms "ProperProxy") in + fun env sigma -> class_info env sigma (Lazy.force r) + + let proper_proj env sigma = + mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs))) + + let proper_type env (sigma,cstrs) = + let l = (proper_class env sigma).cl_impl in + let (sigma, c) = Evarutil.new_global sigma l in + (sigma, cstrs), c + + let proper_proxy_type env (sigma,cstrs) = + let l = (proper_proxy_class env sigma).cl_impl in + let (sigma, c) = Evarutil.new_global sigma l in + (sigma, cstrs), c let proper_proof env evars carrier relation x = - let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in + let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in new_cstr_evar evars env goal let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env @@ -618,7 +622,9 @@ let solve_remaining_by env sigma holes by = in (* Only solve independent holes *) let indep = List.map_filter map holes in - let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in + let ist = { Geninterp.lfun = Id.Map.empty + ; poly = false + ; extra = Geninterp.TacStore.empty } in let solve_tac = match tac with | Genarg.GenArg (Genarg.Glbwit tag, tac) -> Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ()) @@ -798,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev in (* Actual signature found *) let cl_args = [| appmtype' ; signature ; appm |] in - let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type) + let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env) cl_args in let env' = let dosub, appsub = @@ -1308,8 +1314,8 @@ module Strategies = in let evars, proof = let proxy = - if prop then PropGlobal.proper_proxy_type - else TypeGlobal.proper_proxy_type + if prop then PropGlobal.proper_proxy_type env + else TypeGlobal.proper_proxy_type env in let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in new_cstr_evar evars env mty @@ -1790,15 +1796,15 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance atts binders instance fields = +let anew_instance ~pstate atts binders instance fields = let program_mode = atts.program in - new_instance ~program_mode atts.polymorphic + new_instance ~pstate ~program_mode atts.polymorphic binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info -let declare_instance_refl atts binders a aeq n lemma = +let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance atts binders instance + in anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1811,56 +1817,53 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); - let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" - in ignore(anew_instance atts binders instance []); + let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in + let _, pstate = anew_instance ~pstate atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> () + (None, None, None) -> pstate | (Some lemma1, None, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1) + snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 | (None, Some lemma2, None) -> - ignore (declare_instance_sym atts binders a aeq n lemma2) + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (None, None, Some lemma3) -> - ignore (declare_instance_trans atts binders a aeq n lemma3) + snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 | (Some lemma1, Some lemma2, None) -> - ignore (declare_instance_refl atts binders a aeq n lemma1); - ignore (declare_instance_sym atts binders a aeq n lemma2) + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 | (Some lemma1, None, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] | (None, Some lemma2, Some lemma3) -> - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" - in ignore( - anew_instance atts binders instance + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in - let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in - let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) -let proper_projection sigma r ty = +let proper_projection env sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in let ctx, inst = decompose_prod_assum sigma ty in let mor, args = destApp sigma inst in let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in - let app = mkApp (Lazy.force PropGlobal.proper_proj, + let app = mkApp (PropGlobal.proper_proj env sigma, Array.append args [| instarg |]) in it_mkLambda_or_LetIn app ctx @@ -1870,7 +1873,7 @@ let declare_projection n instance_id r = let sigma = Evd.from_env env in let sigma,c = Evd.fresh_global env sigma r in let ty = Retyping.get_type_of env sigma c in - let term = proper_projection sigma c ty in + let term = proper_projection env sigma c ty in let sigma, typ = Typing.type_of env sigma term in let ctx, typ = decompose_prod_assum sigma typ in let typ = @@ -1925,7 +1928,7 @@ let build_morphism_signature env sigma m = rel) cstrs in - let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in + let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in let evd = solve_constraints env !evd in let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in @@ -1939,26 +1942,26 @@ let default_morphism sign m = let evars, _, sign, cstrs = PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign) in - let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in + let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in let evars, mor = resolve_one_typeclass env (goalevars evars) morph in - mor, proper_projection sigma mor morph + mor, proper_projection env sigma mor morph let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid atts binders a aeq t n = +let add_setoid ~pstate atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" - in ignore( - anew_instance atts binders instance + in + snd @@ anew_instance ~pstate atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] let make_tactic name = @@ -1970,7 +1973,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer atts m n = +let add_morphism_infer ~pstate atts m n : Proof_global.t option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); (* NB: atts.program is ignored, program mode automatically set by vernacentries *) @@ -1981,45 +1984,47 @@ let add_morphism_infer atts m n = if Lib.is_modtype () then let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) + add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst); + pstate else let kind = Decl_kinds.Global, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance + Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function - | Globnames.ConstRef cst -> - add_instance (Typeclasses.new_instance - (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info + | Globnames.ConstRef cst -> + add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false + declare_projection n instance_id (ConstRef cst) + | _ -> assert false in let hook = Lemmas.mk_hook hook in - Flags.silently - (fun () -> - Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance); - ignore (Pfedit.by (Tacinterp.interp tac))) () + Flags.silently + (fun () -> + let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () -let add_morphism atts binders m s n = +let add_morphism ~pstate atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance + None + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in + pstate (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 2457b265f0..a200cb5ced 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,18 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : rewrite_attributes -> +val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> unit + constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option -val add_setoid : +val add_setoid : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> unit + Id.t -> Proof_global.t option -val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit +val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option -val add_morphism : - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit +val add_morphism : pstate:Proof_global.t option -> + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index b770b97384..814be64f81 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -48,7 +48,7 @@ let atactic n = else Aentryl (Pltac.tactic_expr, string_of_int n) type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name + 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Extend.symbol -> entry_name (** Quite ad-hoc *) let get_tacentry n m = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index eac84f0543..4398fb14ab 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -138,9 +138,10 @@ let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () (* Signature for interpretation: val_interp and interpretation functions *) -type interp_sign = Geninterp.interp_sign = { - lfun : value Id.Map.t; - extra : TacStore.t } +type interp_sign = Geninterp.interp_sign = + { lfun : value Id.Map.t + ; poly : bool + ; extra : TacStore.t } let extract_trace ist = if is_traced () then match TacStore.get ist.extra f_trace with @@ -544,12 +545,7 @@ let interp_gen kind ist pattern_mode flags env sigma c = let (_, dummy_proofview) = Proofview.init sigma [] in (* Again this is called at times with no open proof! *) - let name, poly = - try - let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in - name, poly - with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false - in + let name, poly = Id.of_string "tacinterp", ist.poly in let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in let (evd,c) = catch_error trace (understand_ltac flags env sigma vars kind) term @@ -566,11 +562,13 @@ let constr_flags () = { fail_evar = true; expand_evars = true; program_mode = false; + polymorphic = false; } (* Interprets a constr; expects evars to be solved *) let interp_constr_gen kind ist env sigma c = - interp_gen kind ist false (constr_flags ()) env sigma c + let flags = { (constr_flags ()) with polymorphic = ist.Geninterp.poly } in + interp_gen kind ist false flags env sigma c let interp_constr = interp_constr_gen WithoutTypeConstraint @@ -582,6 +580,7 @@ let open_constr_use_classes_flags () = { fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } let open_constr_no_classes_flags () = { @@ -590,6 +589,7 @@ let open_constr_no_classes_flags () = { fail_evar = false; expand_evars = true; program_mode = false; + polymorphic = false; } let pure_open_constr_flags = { @@ -598,6 +598,7 @@ let pure_open_constr_flags = { fail_evar = false; expand_evars = false; program_mode = false; + polymorphic = false; } (* Interprets an open constr *) @@ -1021,6 +1022,7 @@ let type_uconstr ?(flags = (constr_flags ())) ltac_idents = closure.idents; ltac_genargs = Id.Map.empty; } in + let flags = { flags with polymorphic = ist.Geninterp.poly } in understand_ltac flags env sigma vars expected_type term end @@ -1146,6 +1148,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (* For extensions *) | TacAlias {loc; v=(s,l)} -> let alias = Tacenv.interp_alias s in + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in let tac l = @@ -1153,8 +1156,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace -> let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in + lfun + ; poly + ; extra = TacStore.set ist.extra f_trace trace } in val_interp ist alias.Tacenv.alias_body >>= fun v -> Ftactic.lift (tactic_of_value ist v) in @@ -1207,12 +1211,13 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ids = extract_ids [] ist.lfun Id.Set.empty in let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> let extra = TacStore.set extra f_trace trace in - let ist = { lfun = Id.Map.empty; extra = extra; } in + let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false (val_interp ~appl ist (Tacenv.interp_ltac r)) @@ -1260,6 +1265,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = (* Interprets an application node *) and interp_app loc ist fv largs : Val.t Ftactic.t = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in if has_type fv (topwit wit_tacvalue) then @@ -1277,9 +1283,11 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = if List.is_empty lvar then begin wrap_error begin - let ist = { - lfun = newlfun; - extra = TacStore.set ist.extra f_trace []; } in + let ist = + { lfun = newlfun + ; poly + ; extra = TacStore.set ist.extra f_trace [] + } in Profile_ltac.do_profile "interp_app" trace ~count_call:false (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) @@ -1317,8 +1325,10 @@ and tactic_of_value ist vle = if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with | VFun (appl,trace,lfun,[],t) -> + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ist = { lfun = lfun; + poly; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) @@ -1388,6 +1398,7 @@ and interp_letin ist llc u = (** [interp_match_success lz ist succ] interprets a single matching success (of type {!Tactic_matching.t}). *) and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in let lctxt = Id.Map.map interp_context context in let hyp_subst = Id.Map.map Value.of_constr terms in @@ -1396,9 +1407,11 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = val_interp ist lhs >>= fun v -> if has_type v (topwit wit_tacvalue) then match to_tacvalue v with | VFun (appl,trace,lfun,[],t) -> - let ist = { - lfun = lfun; - extra = TacStore.set ist.extra f_trace trace; } in + let ist = + { lfun = lfun + ; poly + ; extra = TacStore.set ist.extra f_trace trace + } in let tac = eval_tactic ist t in let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) @@ -1872,7 +1885,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let default_ist () = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in - { lfun = Id.Map.empty; extra = extra } + { lfun = Id.Map.empty; poly = false; extra = extra } let eval_tactic t = Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *) @@ -1912,11 +1925,12 @@ end let interp_tac_gen lfun avoid_ids debug t = + Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in - let ist = { lfun = lfun; extra = extra } in + let ist = { lfun; poly; extra } in let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) @@ -2057,20 +2071,15 @@ let interp_redexp env sigma r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = - let eval lfun env sigma ty tac = + let eval lfun poly env sigma ty tac = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in - let ist = { lfun = lfun; extra; } in + let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* XXX: This depends on the global state which is bad; the hooking - mechanism should be modified. *) - let name, poly = - try - let (_, poly, _) = Proof_global.get_current_persistence () in - let name = Proof_global.get_current_proof_name () in - name, poly - with | Proof_global.NoCurrentProof -> - Id.of_string "ltac_gen", false - in + (* EJGA: We sould also pass the proof name if desired, for now + poly seems like enough to get reasonable behavior in practice + *) + let name, poly = Id.of_string "ltac_gen", poly in + let name, poly = Id.of_string "ltac_gen", poly in let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index d9c80bb835..22a092fa8b 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -39,9 +39,10 @@ module TacStore : Store.S with and type 'a field = 'a Geninterp.TacStore.field (** Signature for interpretation: val\_interp and interpretation functions *) -type interp_sign = Geninterp.interp_sign = { - lfun : value Id.Map.t; - extra : TacStore.t } +type interp_sign = Geninterp.interp_sign = + { lfun : value Id.Map.t + ; poly : bool + ; extra : TacStore.t } open Genintern diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index caaa547a07..e617f3d45e 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x let subst_glob_constr_and_expr subst (c, e) = - (Detyping.subst_glob_constr subst c, e) + (Detyping.subst_glob_constr (Global.env()) subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) @@ -99,7 +99,9 @@ let subst_evaluable subst = let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (bvars,c,p) = - (bvars,subst_glob_constr subst c,subst_pattern subst p) + let env = Global.env () in + let sigma = Evd.from_env env in + (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p) let subst_redexp subst = Redops.map_red_expr_gen diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 52a83a038f..04f3116664 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -370,7 +370,10 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - let sigma, env = Pfedit.get_current_context () in + (* XXX: This hooks into the ExplainErr extension API + so it is tricky to provide the right env for now. *) + let env = Global.env () in + let sigma = Evd.from_env env in Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4c65445b89..d1951cc18d 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) let is_empty _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> - if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail + if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test sigma (assoc_var "X1" ist) then idtac else fail + if test genv sigma (assoc_var "X1" ist) then idtac else fail let bugged_is_binary sigma t = isApp sigma t && @@ -121,23 +123,25 @@ let bugged_is_binary sigma t = (** Dealing with conjunction *) let is_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) && - is_conjunction sigma + is_conjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind then idtac else fail let flatten_contravariant_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_conjunction sigma + match match_with_conjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with @@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist = (** Dealing with disjunction *) let is_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) && - is_disjunction sigma + is_disjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t then idtac else fail let flatten_contravariant_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_disjunction sigma + match match_with_disjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with |