diff options
Diffstat (limited to 'plugins/ltac')
46 files changed, 516 insertions, 528 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 0a13a20a9..07b8746fb 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -8,15 +8,14 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Util -open Names open Locus open Misctypes open Genredexpr open Stdarg open Extraargs - -open Sigma.Notations +open Names DECLARE PLUGIN "coretactics" @@ -160,12 +159,12 @@ END (** Split *) let rec delayed_list = function -| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma } +| [] -> fun _ sigma -> (sigma, []) | x :: l -> - { Tacexpr.delayed = fun env sigma -> - let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in - let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in - Sigma (x :: l, sigma, p +> q) } + fun env sigma -> + let (sigma, x) = x env sigma in + let (sigma, l) = delayed_list l env sigma in + (sigma, x :: l) TACTIC EXTEND split [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] @@ -308,7 +307,7 @@ let initial_atomic () = let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in let iter (s, t) = let body = TacAtom (Loc.tag t) in - Tacenv.register_ltac false false (Id.of_string s) body + Tacenv.register_ltac false false (Names.Id.of_string s) body in let () = List.iter iter [ "red", TacReduce(Red false,nocl); @@ -318,7 +317,7 @@ let initial_atomic () = "intros", TacIntroPattern (false,[]); ] in - let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in + let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in List.iter iter [ "idtac",TacId []; "fail", TacFail(TacLocal,ArgArg 0,[]); diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index bf84f61a5..a299e11f8 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Names open Term @@ -16,8 +17,6 @@ open Tacexpr open Refiner open Evd open Locus -open Sigma.Notations -open Proofview.Notations open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -81,29 +80,26 @@ let instantiate_tac_by_name id c = let let_evar name typ = let src = (Loc.tag Evar_kinds.GoalEvar) in - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let sigma = ref sigma in let _ = Typing.e_sort_of env sigma typ in let sigma = !sigma in let id = match name with - | Names.Anonymous -> + | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) - | Names.Name id -> id + | Name.Name id -> id in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in - let tac = - (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) - in - Sigma (tac, sigma, p) - end } - + let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) + end + let hget_evar n = let open EConstr in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in let evl = evar_list sigma concl in @@ -112,6 +108,5 @@ let hget_evar n = if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in - Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) - end } - + Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl)) + end diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index cfe747665..7c734cd9a 100644 --- a/plugins/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Tacexpr open Locus diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index fdb8d3461..44f33ab80 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API +open Grammar_API open Pp open Genarg open Stdarg @@ -83,7 +85,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Nameops.pr_id id + | ArgVar (loc, id) -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -199,8 +201,8 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id) -let pr_place _ _ _ = pr_gen_place Nameops.pr_id +let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () let intern_place ist = function @@ -236,7 +238,7 @@ ARGUMENT EXTEND hloc END -let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m +let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m ARGUMENT EXTEND rename TYPED AS ident * ident diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 9b4167512..b2b3f8b6b 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Tacexpr open Names open Constrexpr diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index d68139a4b..18d7b818c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API +open Grammar_API open Pp open Genarg open Stdarg @@ -24,7 +26,6 @@ open Util open Termops open Equality open Misctypes -open Sigma.Notations open Proofview.Notations DECLARE PLUGIN "extratactics" @@ -80,12 +81,12 @@ let induction_arg_of_quantified_hyp = function ElimOnIdent and not as "constr" *) let mytclWithHoles tac with_evars c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' - end } + end let elimOnConstrWithHoles tac with_evars c = Tacticals.New.tclDELAYEDWITHHOLES with_evars c @@ -115,7 +116,7 @@ END let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> - discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } + discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) let injection_main with_evars c = elimOnConstrWithHoles (injClause None) with_evars c @@ -147,7 +148,7 @@ END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> - injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } + injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -306,7 +307,8 @@ let project_hint pri l2r r = | _ -> assert false in let p = if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in - let p = EConstr.of_constr @@ Universes.constr_of_global p in + let sigma, p = Evd.fresh_global env sigma p in + let p = EConstr.of_constr p in let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in let c = it_mkLambda_or_LetIn (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in @@ -353,23 +355,22 @@ let constr_flags () = { Pretyping.expand_evars = true } let refine_tac ist simple with_classes c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in - let update = { run = fun sigma -> - let Sigma (c, sigma, p) = c.delayed env sigma in - Sigma (c, sigma, p) - } in + let update = begin fun sigma -> + c env sigma + end in let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> Proofview.shelve_unifiable - end } + end TACTIC EXTEND refine | [ "refine" uconstr(c) ] -> @@ -463,8 +464,8 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] -| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ] +| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ] END TACTIC EXTEND instantiate @@ -515,7 +516,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity : bool * Constr.constr -> obj = +let inTransitivity : bool * Term.constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); @@ -636,7 +637,7 @@ let subst_var_with_hole occ tid t = else (incr locref; CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true), + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), Misctypes.IntroAnonymous, None))) else x | c -> map_glob_constr_left_to_right substrec c in @@ -648,13 +649,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec = function - | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } -> + | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } -> decr occref; if Int.equal !occref 0 then tc else (incr locref; CAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) | c -> map_glob_constr_left_to_right substrec c in substrec t @@ -662,9 +663,8 @@ let subst_hole_with_term occ tc t = open Tacmach let hResolve id c occ t = - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let sigma = Sigma.to_evar_map sigma in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in let env_ids = Termops.ids_of_context env in @@ -683,11 +683,9 @@ let hResolve id c occ t = let t_constr = EConstr.of_constr t_constr in let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in - let tac = - (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) + end let hResolve_auto id c t = let rec resolve_auto n = @@ -725,17 +723,16 @@ END exception Found of unit Proofview.tactic let rewrite_except h = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) hyps - end } + end let refl_equal = let coq_base_constant s = - Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s in function () -> (coq_base_constant "eq_refl") @@ -745,28 +742,29 @@ let refl_equal = should be replaced by a call to the tactic but I don't know how to call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))]; - Proofview.Goal.enter { enter = begin fun gl -> + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in + let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in change_concl c - end }; + end; simplest_case a] - end } + end let case_eq_intros_rewrite x = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let n' = nb_prod (Tacmach.New.project gl) concl in @@ -775,9 +773,9 @@ let case_eq_intros_rewrite x = Tacticals.New.tclDO (n'-n-1) intro; introduction h; rewrite_except h] - end } + end ] - end } + end let rec find_a_destructable_match sigma t = let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in @@ -801,15 +799,15 @@ let destauto t = with Found tac -> tac let destauto_in id = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype - end } + end TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ] +| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ] | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] END @@ -821,21 +819,21 @@ END (**********************************************************************) 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) } ] +| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] END (* ********************************************************************* *) let eq_constr x y = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let evd = Tacmach.New.project gl in match EConstr.eq_constr_universes evd x y with | Some _ -> Proofview.tclUNIT () | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end } + end TACTIC EXTEND constr_eq | [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] @@ -1081,7 +1079,7 @@ TACTIC EXTEND guard END let decompose l c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let to_ind c = if isInd sigma c then fst (destInd sigma c) @@ -1089,7 +1087,7 @@ let decompose l c = in let l = List.map to_ind l in Elim.h_decompose l c - end } + end TACTIC EXTEND decompose | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 18334dafe..c7ec26967 100644 --- a/plugins/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API + val discrHyp : Names.Id.t -> unit Proofview.tactic val injHyp : Names.Id.t -> unit Proofview.tactic diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 50e8255a6..dfd8e88a9 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API +open Grammar_API open Pp open Genarg open Stdarg @@ -15,8 +17,6 @@ open Pcoq.Prim open Pcoq.Constr open Pltac open Hints -open Tacexpr -open Names DECLARE PLUGIN "g_auto" @@ -49,10 +49,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - let map c = { delayed = fun env sigma -> - let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in - Sigma.Sigma (c, sigma, p) - } in + let map c env sigma = c env sigma in List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 23ce368ee..905cfd02a 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -8,10 +8,10 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Class_tactics open Stdarg open Tacarg -open Names DECLARE PLUGIN "g_class" @@ -102,18 +102,18 @@ let rec eq_constr_mod_evars sigma x y = | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y let progress_evars t = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let check = - Proofview.Goal.enter { enter = begin fun gl' -> + Proofview.Goal.enter begin fun gl' -> let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars sigma concl newconcl then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () - end } + end in t <*> check - end } + end TACTIC EXTEND progress_evars [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 679aa1127..570cd4e69 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -14,8 +14,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API open Eqdecide -open Names DECLARE PLUGIN "g_eqdecide" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 36ac10bfe..4bab31b85 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -8,6 +8,9 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API +open Grammar_API + DECLARE PLUGIN "ltac_plugin" open Util @@ -228,8 +231,8 @@ GEXTEND Gram | "multimatch" -> General ] ] ; input_fun: - [ [ "_" -> Anonymous - | l = ident -> Name l ] ] + [ [ "_" -> Name.Anonymous + | l = ident -> Name.Name l ] ] ; let_clause: [ [ id = identref; ":="; te = tactic_expr -> @@ -396,7 +399,7 @@ let pr_ltac_selector = function | SelectNth i -> int i ++ str ":" | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str "]" ++ str ":" -| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" +| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector @@ -466,14 +469,14 @@ let pr_ltac_production_item = function | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) in - str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")" + str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ] | [ ident(nt) ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation @@ -496,7 +499,7 @@ let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> Nameops.pr_id id, false, body + | TacticDefinition ((_,id), body) -> Id.print id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = @@ -504,8 +507,8 @@ let pr_tacdef_body tacdef_body = | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in id ++ - prlist (function Anonymous -> str " _" - | Name id -> spc () ++ Nameops.pr_id id) idl + prlist (function Name.Anonymous -> str " _" + | Name.Name id -> spc () ++ Id.print id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ Pptactic.pr_raw_tactic body diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 4dceb0331..18e62a211 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,8 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) - +open API +open Grammar_API open Libnames open Constrexpr open Constrexpr_ops diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 5adf8475a..e6ddc5cc1 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -10,6 +10,8 @@ (* Syntax for rewriting with strategies *) +open API +open Grammar_API open Names open Misctypes open Locus @@ -18,7 +20,6 @@ open Glob_term open Geninterp open Extraargs open Tacmach -open Proofview.Notations open Rewrite open Stdarg open Pcoq.Vernac_ @@ -123,7 +124,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP @@ -132,7 +133,7 @@ let clsubstitute o c = | Some id when is_tac id -> Tacticals.New.tclIDTAC | _ -> cl_rewrite_clause c o AllOccurrences cl) (None :: List.map (fun id -> Some id) hyps) - end } + end TACTIC EXTEND substitute | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 1404b1c1f..a971fc79f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Pp open CErrors open Util @@ -475,7 +477,7 @@ GEXTEND Gram | -> None ] ] ; as_name: - [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] + [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ] ; by_tactic: [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac @@ -538,43 +540,69 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) | IDENT "pose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) + | IDENT "epose"; (id,b) = bindings_with_parameters -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) + | IDENT "epose"; b = constr; na = as_name -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None)) + | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) + | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None)) | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e)) + | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) (* Alternative syntax for "pose proof c as id" *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + c = lconstr; ")" -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) + | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c)) | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c)) + | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c)) | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c)) + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c)) + | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> + TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c)) | IDENT "generalize"; c = constr -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)]) + TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in + let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l))) | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index 7e979d269..84c5d3a44 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Pcoq (* Main entry for extensions *) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 810e1ec39..9261a11c7 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -8,6 +8,8 @@ (** Ltac parsing entries *) +open API +open Grammar_API open Loc open Names open Pcoq diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a001c6a2b..8300a55e3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Pp open Names open Namegen @@ -161,28 +162,6 @@ type 'a extra_genarg_printer = | AnonHyp n -> int n | NamedHyp id -> pr_id id - let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - - let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc prc l) - | ExplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) - | NoBindings -> mt () - - let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - let pr_clear_flag clear_flag pp x = match clear_flag with | Some false -> surround (pp x) @@ -190,7 +169,7 @@ type 'a extra_genarg_printer = | None -> pp x let pr_with_bindings prc prlc (c,bl) = - prc c ++ pr_bindings prc prlc bl + prc c ++ Miscprint.pr_bindings prc prlc bl let pr_with_bindings_arg prc prlc (clear_flag,c) = pr_clear_flag clear_flag (pr_with_bindings prc prlc) c @@ -356,41 +335,17 @@ type 'a extra_genarg_printer = | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = - if !Flags.in_debugger then pr_kn kn + if !Flags.in_debugger then KerName.print kn else try pr_qualid (Nametab.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) - str "<" ++ pr_kn kn ++ str ">" + str "<" ++ KerName.print kn ++ str ">" let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) - let pr_esubst prc l = - let pr_qhyp = function - (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,(NamedHyp id,c)) -> - str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" - in - prlist_with_sep spc pr_qhyp l - - let pr_bindings_gen for_ex prc prlc = function - | ImplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - prlist_with_sep spc prc l) - | ExplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - pr_esubst prlc l) - | NoBindings -> mt () - - let pr_bindings prc prlc = pr_bindings_gen false prc prlc - - let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl @@ -527,7 +482,7 @@ type 'a extra_genarg_printer = | SelectNth i -> int i ++ str ":" | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str "]" ++ str ":" - | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" let pr_lazy = function @@ -571,7 +526,7 @@ type 'a extra_genarg_printer = str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar n = spc () ++ pr_name n + let pr_funvar n = spc () ++ Name.print n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ @@ -582,7 +537,7 @@ type 'a extra_genarg_printer = hv 0 (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) - | [] -> anomaly (Pp.str "LetIn must declare at least one binding") + | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = hv 0 (str "[ " ++ @@ -768,15 +723,15 @@ type 'a extra_genarg_printer = primitive "cofix" ++ spc () ++ pr_id id ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l ) - | TacAssert (b,Some tac,ipat,c) -> + | TacAssert (ev,b,Some tac,ipat,c) -> hov 1 ( - primitive (if b then "assert" else "enough") ++ + primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++ pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac ) - | TacAssert (_,None,ipat,c) -> + | TacAssert (ev,_,None,ipat,c) -> hov 1 ( - primitive "pose proof" + primitive (if ev then "epose proof" else "pose proof") ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ) | TacGeneralize l -> @@ -786,11 +741,11 @@ type 'a extra_genarg_printer = pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> - hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) - | TacLetTac (na,c,cl,b,e) -> + | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl -> + hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c) + | TacLetTac (ev,na,c,cl,b,e) -> hov 1 ( - (if b then primitive "set" else primitive "remember") ++ + primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++ (if b then pr_pose pr.pr_constr pr.pr_lconstr na c else pr_pose_as_style pr.pr_constr na c) ++ pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++ @@ -1225,11 +1180,10 @@ let declare_extra_genarg_pprule wit (** Registering *) -let run_delayed c = - Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma } +let run_delayed c = c (Global.env ()) Evd.empty let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g)) + | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) | clear_flag,ElimOnAnonHyp n as x -> x | clear_flag,ElimOnIdent id as x -> x @@ -1249,7 +1203,7 @@ let () = wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c)))); + (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1280,13 +1234,13 @@ let () = (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 wit_bindings - (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); + (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it))); + (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 19bdf2d49..519283759 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -9,6 +9,7 @@ (** This module implements pretty-printers for tactic_expr syntactic objects and their subcomponents. *) +open API open Pp open Genarg open Geninterp @@ -106,10 +107,6 @@ val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds -val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 3ff7b53c7..020b3048f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Unicode open Pp open Printer @@ -113,7 +114,7 @@ let rec to_ltacprof_tactic m xml = children = List.fold_left to_ltacprof_tactic M.empty xs; } in M.add name node m - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof_tactic XML.") let to_ltacprof_results xml = let open Xml_datatype in @@ -125,7 +126,7 @@ let to_ltacprof_results xml = max_total = 0.0; local = 0.0; children = List.fold_left to_ltacprof_tactic M.empty xs } - | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML") + | _ -> CErrors.anomaly Pp.(str "Malformed ltacprof XML.") let feedback_results results = Feedback.(feedback @@ -246,7 +247,7 @@ let string_of_call ck = (match ck with | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) (Tacexpr.TacAtom (Loc.tag te))) diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index e5e2e4197..09fc549c6 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API + (** Ltac profiling primitives *) val do_profile : diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 8cb76d81c..83fb6963b 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -10,6 +10,7 @@ (** Ltac profiling entrypoints *) +open API open Profile_ltac open Stdarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 966b11d0e..3927ca7ce 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Pp open CErrors @@ -33,7 +34,6 @@ open Environ open Termops open EConstr open Libnames -open Sigma.Notations open Proofview.Notations open Context.Named.Declaration @@ -66,9 +66,7 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in - let evd = Sigma.to_evar_map sigma in + let (evd, c) = Evarutil.new_global evd (Lazy.force gr) in (evd, cstrs), c (** Utility for dealing with polymorphic applications *) @@ -89,9 +87,7 @@ let cstrevars evars = snd evars let new_cstr_evar (evd,cstrs) env t = let s = Typeclasses.set_resolvable Evd.Store.empty false in - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in - let evd' = Sigma.to_evar_map evd' in + let (evd', t) = Evarutil.new_evar ~store:s env evd t in let ev, _ = destEvar evd' t in (evd', Evar.Set.add ev cstrs), t @@ -176,17 +172,13 @@ end) = struct let proper_type = let l = lazy (Lazy.force proper_class).cl_impl in fun (evd,cstrs) -> - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let evd = Sigma.to_evar_map sigma in + 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 sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in - let evd = Sigma.to_evar_map sigma in + let (evd, c) = Evarutil.new_global evd (Lazy.force l) in (evd, cstrs), c let proper_proof env evars carrier relation x = @@ -236,7 +228,7 @@ end) = struct let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") - | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") + | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.") | _, [] -> (match finalcstr with | None | Some (_, None) -> @@ -357,9 +349,7 @@ end) = struct (try let params, args = Array.chop (Array.length args - 2) args in let env' = push_rel_context rels env in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in - let evars = Sigma.to_evar_map evars in + let (evars, (evar, _)) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in @@ -419,9 +409,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let sigma = Sigma.Unsafe.of_evar_map evd in - let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in - let evd = Sigma.to_evar_map sigma in + let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end @@ -439,7 +427,7 @@ let split_head = function | [] -> assert(false) let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = - pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -751,17 +739,23 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } let get_opt_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None -let make_eq () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) -let make_eq_refl () = -(*FIXME*) EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ())) +let new_global (evars, cstrs) gr = + let (sigma,c) = Evarutil.new_global evars gr in + (sigma, cstrs), c -let get_rew_prf r = match r.rew_prf with - | RewPrf (rel, prf) -> rel, prf +let make_eq sigma = + new_global sigma (Coqlib.build_coq_eq ()) +let make_eq_refl sigma = + new_global sigma (Coqlib.build_coq_eq_refl ()) + +let get_rew_prf evars r = match r.rew_prf with + | RewPrf (rel, prf) -> evars, (rel, prf) | RewCast c -> - let rel = mkApp (make_eq (), [| r.rew_car |]) in - rel, mkCast (mkApp (make_eq_refl (), [| r.rew_car; r.rew_from |]), - c, mkApp (rel, [| r.rew_from; r.rew_to |])) + let evars, eq = make_eq evars in + let evars, eq_refl = make_eq_refl evars in + let rel = mkApp (eq, [| r.rew_car |]) in + evars, (rel, mkCast (mkApp (eq_refl, [| r.rew_car; r.rew_from |]), + c, mkApp (rel, [| r.rew_from; r.rew_to |]))) let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation @@ -827,7 +821,8 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ snd (get_rew_prf r); r.rew_to; x ] @ acc, subst, evars, + let evars, proof = get_rew_prf evars r in + [ snd proof; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then @@ -847,7 +842,8 @@ let apply_constraint env avoid car rel prf cstr res = | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res let coerce env avoid cstr res = - let rel, prf = get_rew_prf res in + let evars, (rel, prf) = get_rew_prf res.rew_evars res in + let res = { res with rew_evars = evars } in apply_constraint env avoid res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = @@ -868,8 +864,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let rel, prf = get_rew_prf res in - let res = Success (apply_constraint env unfresh rew.rew_car rel prf cstr res) in + let res = Success (coerce env unfresh cstr res) in (occ, res) } @@ -962,7 +957,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when eq_constant (fst (destConst sigma f')) sk -> + | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta sigma (mkApp (v, args)) @@ -1231,9 +1226,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> - let rel, prf = get_rew_prf r in - Success (apply_constraint env unfresh r.rew_car rel prf (prop,cstr) r) + | Success r -> Success (coerce env unfresh (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail @@ -1378,7 +1371,7 @@ module Strategies = fail cs let inj_open hint = (); fun sigma -> - let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in + let ctx = UState.of_context_set hint.Autorewrite.rew_ctx in let sigma = Evd.merge_universe_context sigma ctx in (sigma, (EConstr.of_constr hint.Autorewrite.rew_lemma, NoBindings)) @@ -1401,15 +1394,14 @@ module Strategies = let reduce (r : Redexpr.red_expr) : 'a pure_strategy = { strategy = fun { state = state ; env = env ; term1 = t ; ty1 = ty ; cstr = cstr ; evars = evars } -> let rfn, ckind = Redexpr.reduction_of_red_expr env r in - let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in - let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma t in - let evars' = Sigma.to_evar_map sigma in - if Termops.eq_constr evars' t' t then + let sigma = goalevars evars in + let (sigma, t') = rfn env sigma t in + if Termops.eq_constr sigma t' t then state, Identity else state, Success { rew_car = ty; rew_from = t; rew_to = t'; rew_prf = RewCast ckind; - rew_evars = evars', cstrevars evars } + rew_evars = sigma, cstrevars evars } } let fold_glob c : 'a pure_strategy = { strategy = @@ -1419,7 +1411,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - user_err Pp.(str "fold: the term is not unfoldable !") + user_err Pp.(str "fold: the term is not unfoldable!") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -1480,7 +1472,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = - if is_prop_sort sort then true, app_poly_sort true env evars impl [||] + if Sorts.is_prop sort then true, app_poly_sort true env evars impl [||] else false, app_poly_sort false env evars TypeGlobal.arrow [||] in match is_hyp with @@ -1536,7 +1528,7 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with insert_dependent env sigma decl (ndecl :: accu) rem let assert_replacing id newt tac = - let prf = Proofview.Goal.enter { enter = begin fun gl -> + let prf = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1547,17 +1539,17 @@ let assert_replacing id newt tac = | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in - Refine.refine ~unsafe:false { run = begin fun sigma -> - let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in - let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in + Refine.refine ~unsafe:false begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env' sigma concl in + let (sigma, ev') = Evarutil.new_evar env sigma newt in let map d = let n = NamedDecl.get_id d in if Id.equal n id then ev' else mkVar n in - let (e, _) = destEvar (Sigma.to_evar_map sigma) ev in - Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q) - end } - end } in + let (e, _) = destEvar sigma ev in + (sigma, mkEvar (e, Array.map_of_list map nc)) + end + end in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = @@ -1581,7 +1573,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ - Refine.refine ~unsafe:false { run = fun h -> Sigma.here p h }; + Refine.refine ~unsafe:false (fun h -> (h,p)); Proofview.Unsafe.tclNEWGOALS gls; ] in Proofview.Unsafe.tclEVARS undef <*> @@ -1592,19 +1584,19 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let make = { run = begin fun sigma -> - let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in - Sigma (mkApp (p, [| ev |]), sigma, q) - end } in + let make = begin fun sigma -> + let (sigma, ev) = Evarutil.new_evar env sigma newt in + (sigma, mkApp (p, [| ev |])) + end in Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls - end } + end | None, None -> Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -1632,7 +1624,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = with | PretypeError (env, evd, (UnsatisfiableConstraints _ as e)) -> raise (RewriteFailure (Himsg.explain_pretype_error env evd e)) - end } + end let tactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () @@ -1973,7 +1965,7 @@ let add_morphism_infer glob m n = if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,Evd.evar_context_universe_context uctx),None), + (None,poly,(instance,UState.context uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance @@ -2087,7 +2079,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let abs, evd, res, sort = get_hyp gl (c,l) cl l2r in let unify env evars t = unify_abs res l2r sort env evars t in let app = apply_rule unify occs in @@ -2109,7 +2101,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = | RewriteFailure e -> tclFAIL 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) - end } + end let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite @@ -2121,7 +2113,7 @@ let not_declared env sigma ty rel = str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") let setoid_proof ty fn fallback = - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -2150,7 +2142,7 @@ let setoid_proof ty fn fallback = | e' -> Proofview.tclZERO ~info e' end end - end } + end let tac_open ((evm,_), c) tac = (tclTHEN (Proofview.Unsafe.tclEVARS evm) (tac c)) @@ -2190,7 +2182,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = let open Tacmach.New in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let ctype = pf_unsafe_type_of gl (mkVar id) in let binders,concl = decompose_prod_assum sigma ctype in @@ -2207,7 +2199,7 @@ let setoid_symmetry_in id = (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) - end } + end let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 6683d753b..d7f92fd6e 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names -open Constr open Environ open EConstr open Constrexpr @@ -38,7 +38,7 @@ type ('constr,'redexpr) strategy_ast = type rewrite_proof = | RewPrf of constr * constr - | RewCast of cast_kind + | RewCast of Term.cast_kind type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 42552c484..2c9bf14be 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -8,6 +8,7 @@ (** Generic arguments based on Ltac. *) +open API open Genarg open Geninterp open Tacexpr diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bfa423db2..e82cb516c 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Genarg open Tacexpr open Constrexpr diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index e037bb4b2..117a16b0a 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Names open Term @@ -131,8 +132,8 @@ let coerce_var_to_ident fresh env sigma v = let coerce_to_ident_not_fresh env sigma v = let g = sigma in let id_of_name = function - | Names.Anonymous -> Id.of_string "x" - | Names.Name x -> x in + | Name.Anonymous -> Id.of_string "x" + | Name.Name x -> x in let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 9883c03c4..2c02171d0 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Names open EConstr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 75f89a81e..270225e23 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Pp open CErrors open Util @@ -417,7 +419,7 @@ let is_defined_tac kn = let warn_unusable_identifier = CWarnings.create ~name:"unusable-identifier" ~category:"parsing" - (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++ + (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++ strbrk "may be unusable because of a conflict with a notation.") let register_ltac local tacl = @@ -425,7 +427,7 @@ let register_ltac local tacl = match tactic_body with | Tacexpr.TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in - let id_pp = pr_id id in + let id_pp = Id.print id in let () = if is_defined_tac kn then CErrors.user_err ?loc (str "There is already an Ltac named " ++ id_pp ++ str".") @@ -473,7 +475,7 @@ let register_ltac local tacl = let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; - Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; let name = Nametab.shortest_qualid_of_tactic kn in @@ -502,7 +504,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg n = spc () ++ pr_name n in + let pr_ltac_fun_arg n = spc () ++ Name.print n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 07aa7ad82..c5223052c 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -8,6 +8,8 @@ (** Ltac toplevel command entries. *) +open API +open Grammar_API open Vernacexpr open Tacexpr diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index e3c2b4ad5..14b5e00c7 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Pp open Names @@ -24,7 +25,7 @@ let register_alias key tac = let interp_alias key = try KNmap.find key !alias_map - with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) + with Not_found -> CErrors.anomaly (str "Unknown tactic alias: " ++ KerName.print key ++ str ".") let check_alias key = KNmap.mem key !alias_map diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index d1e2a7bbe..2295852ce 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Tacexpr open Geninterp diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index bf760e7bb..9b6ac8a9a 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Loc open Names open Constrexpr @@ -117,8 +118,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Constr_matching.binding_bound_vars type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern -type 'a delayed_open = 'a Tactypes.delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } +type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open @@ -141,10 +141,10 @@ type 'a gen_atomic_tactic_expr = | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of - bool * 'tacexpr option option * + evars_flag * bool * 'tacexpr option option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * + | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option (* Derived basic tactics *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index e431a13bc..bc1dd26d9 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Pattern open Pp open Genredexpr @@ -14,7 +16,6 @@ open Tacred open CErrors open Util open Names -open Nameops open Libnames open Globnames open Nametab @@ -189,7 +190,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -198,7 +199,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c in (c',if !strict_check then None else Some c) @@ -489,17 +490,17 @@ let rec intern_atomic lf ist x = | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) - | TacAssert (b,otac,ipat,c) -> - TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac, + | TacAssert (ev,b,otac,ipat,c) -> + TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac, Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen false (not (Option.is_empty otac)) ist c) | TacGeneralize cl -> TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, intern_name lf ist na) cl) - | TacLetTac (na,c,cls,b,eqpat) -> + | TacLetTac (ev,na,c,cls,b,eqpat) -> let na = intern_name lf ist na in - TacLetTac (na,intern_constr ist c, + TacLetTac (ev,na,intern_constr ist c, (clause_app (intern_hyp_location ist) cls),b, (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat)) @@ -718,7 +719,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg n = spc () ++ pr_name n +let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 8ad52ca02..1841ab42b 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Pp open Names open Tacexpr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a9ec779d1..9d8094205 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Constrintern open Patternops open Pp @@ -37,7 +39,6 @@ open Misctypes open Locus open Tacintern open Taccoerce -open Sigma.Notations open Proofview.Notations open Context.Named.Declaration @@ -91,7 +92,7 @@ type value = Val.t (** Abstract application, to print ltac functions *) type appl = | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.kernel_name * Val.t list) list + | GlbAppl of (Names.KerName.t * Val.t list) list (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with @@ -256,7 +257,7 @@ let pr_closure env ist body = let pr_sep () = fnl () in let pr_iarg (id, arg) = let arg = pr_argument_type arg in - hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg) + hov 0 (Id.print id ++ spc () ++ str ":" ++ spc () ++ arg) in let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in pp_body ++ fnl() ++ str "in environment " ++ fnl() ++ pp_iargs @@ -313,7 +314,7 @@ let append_trace trace v = let coerce_to_tactic loc id v = let v = Value.normalize v in let fail () = user_err ?loc - (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") + (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then @@ -368,7 +369,7 @@ let debugging_exception_step ist signal_anomaly e pp = pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) let error_ltac_variable ?loc id env v s = - user_err ?loc (str "Ltac variable " ++ pr_id id ++ + user_err ?loc (str "Ltac variable " ++ Id.print id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") @@ -379,7 +380,7 @@ let try_interp_ltac_var coerce ist env (loc,id) = let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time") + with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.") let interp_ident ist env sigma id = try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) @@ -402,7 +403,7 @@ let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> user_err ?loc:(fst locid) ~hdr:"interp_int" - (str "Unbound variable " ++ pr_id (snd locid) ++ str".") + (str "Unbound variable " ++ Id.print (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -577,57 +578,47 @@ let extract_ltac_constr_context ist env sigma = (** Significantly simpler than [interp_constr], to interpret an untyped constr, it suffices to adjoin a closure environment. *) -let interp_uconstr ist env sigma = function - | (term,None) -> - { closure = extract_ltac_constr_context ist env sigma; term } - | (_,Some ce) -> - let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in +let interp_glob_closure ist env sigma ?(kind=WithoutTypeConstraint) ?(pattern_mode=false) (term,term_expr_opt) = + let closure = extract_ltac_constr_context ist env sigma in + match term_expr_opt with + | None -> { closure ; term } + | Some term_expr -> + (* If at toplevel (term_expr_opt<>None), the error can be due to + an incorrect context at globalization time: we retype with the + now known intros/lettac/inversion hypothesis names *) + let constr_context = + Id.Set.union + (Id.Map.domain closure.typed) + (Id.Map.domain closure.untyped) + in let ltacvars = { - Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped)); + ltac_vars = constr_context; ltac_bound = Id.Map.domain ist.lfun; ltac_extra = Genintern.Store.empty; } in - { closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce } + { closure ; term = intern_gen kind ~pattern_mode ~ltacvars env term_expr } + +let interp_uconstr ist env sigma c = interp_glob_closure ist env sigma c -let interp_gen kind ist allow_patvar flags env sigma (c,ce) = - let constrvars = extract_ltac_constr_context ist env sigma in +let interp_gen kind ist pattern_mode flags env sigma c = + let kind_for_intern = match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in + let { closure = constrvars ; term } = + interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { Pretyping.ltac_constrs = constrvars.typed; Pretyping.ltac_uconstrs = constrvars.untyped; Pretyping.ltac_idents = constrvars.idents; Pretyping.ltac_genargs = ist.lfun; } in - let c = match ce with - | None -> c - (* If at toplevel (ce<>None), the error can be due to an incorrect - context at globalization time: we retype with the now known - intros/lettac/inversion hypothesis names *) - | Some c -> - let constr_context = - Id.Set.union - (Id.Map.domain constrvars.typed) - (Id.Set.union - (Id.Map.domain constrvars.untyped) - (Id.Map.domain constrvars.idents)) - in - let ltacvars = { - ltac_vars = constr_context; - ltac_bound = Id.Map.domain ist.lfun; - ltac_extra = Genintern.Store.empty; - } in - let kind_for_intern = - match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in - intern_gen kind_for_intern ~allow_patvar ~ltacvars env c - in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do this with the kludge of an empty proofview, and rely on the invariant that running the tactic returned by push_trace does not modify sigma. *) let (_, dummy_proofview) = Proofview.init sigma [] in - let (trace,_,_,_) = Proofview.apply env (push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist) dummy_proofview in + let (trace,_,_,_) = Proofview.apply 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) c + catch_error trace (understand_ltac flags env sigma vars kind) term in (* spiwack: to avoid unnecessary modifications of tacinterp, as this function already use effect, I call [run] hoping it doesn't mess @@ -672,12 +663,12 @@ let pure_open_constr_flags = { expand_evars = false } (* Interprets an open constr *) -let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c = - let flags = - if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags () - else open_constr_use_classes_flags () in +let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c = interp_gen expected_type ist false flags env sigma c +let interp_open_constr_with_classes ?(expected_type=WithoutTypeConstraint) ist env sigma c = + interp_gen expected_type ist false (open_constr_use_classes_flags ()) env sigma c + let interp_pure_open_constr ist = interp_gen WithoutTypeConstraint ist false pure_open_constr_flags @@ -777,9 +768,7 @@ let interp_may_eval f ist env sigma = function let (sigma,redexp) = interp_red_expr ist env sigma r in let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in - (Sigma.to_evar_map sigma, c) + redfun env sigma c_interp | ConstrContext ((loc,s),c) -> (try let (sigma,ic) = f ist env sigma c in @@ -793,7 +782,7 @@ let interp_may_eval f ist env sigma = function with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" - (str "Unbound context identifier" ++ pr_id s ++ str".")) + (str "Unbound context identifier" ++ Id.print s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in @@ -839,12 +828,12 @@ let rec message_of_value v = Ftactic.return (str "<tactic>") else if has_type v (topwit wit_constr) then let v = out_gen (topwit wit_constr) v in - Ftactic.enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end } + Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end } + end else if has_type v (topwit wit_unit) then Ftactic.return (str "()") else if has_type v (topwit wit_int) then @@ -852,24 +841,24 @@ let rec message_of_value v = else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in let print env sigma c = - let (c, sigma) = Tactics.run_delayed env sigma c in + let (sigma, c) = c env sigma in pr_econstr_env env sigma c in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end } + end else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end } + Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end else if has_type v (topwit wit_uconstr) then let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> Ftactic.return (pr_closed_glob_env (pf_env gl) (project gl) c) - end } + end else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in - Ftactic.enter { enter = begin fun gl -> Ftactic.return (pr_id id) end } + Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> @@ -884,7 +873,7 @@ let interp_message_token ist = function | MsgIdent (loc,id) -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with - | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (pr_id id ++ str" not found.")) + | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) | Some v -> message_of_value v let interp_message ist l = @@ -915,11 +904,7 @@ and interp_intro_pattern_action ist env sigma = function let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in sigma, IntroInjection l | IntroApplyOn ((loc,c),ipat) -> - let c = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } in + let c env sigma = interp_open_constr ist env sigma c in let sigma,ipat = interp_intro_pattern ist env sigma ipat in sigma, IntroApplyOn ((loc,c),ipat) | IntroWildcard | IntroRewrite _ as x -> sigma, x @@ -1013,37 +998,31 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = Loc.merge_opt loc1 loc2 in - let f = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in - Sigma.Unsafe.of_pair (c, sigma) - } in - (loc,f) + let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + (loc,f) let interp_destruction_arg ist gl arg = match arg with | keep,ElimOnConstr c -> - keep,ElimOnConstr { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } + keep,ElimOnConstr begin fun env sigma -> + interp_open_constr_with_bindings ist env sigma c + end | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err ?loc - (strbrk "Cannot coerce " ++ pr_id id ++ + (strbrk "Cannot coerce " ++ Id.print id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') else - (keep, ElimOnConstr { delayed = begin fun env sigma -> - try Sigma.here (constr_of_id env id', NoBindings) sigma + (keep, ElimOnConstr begin fun env sigma -> + try (sigma, (constr_of_id env id', NoBindings)) with Not_found -> user_err ?loc ~hdr:"interp_destruction_arg" ( - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") - end }) + Id.print id ++ strbrk " binds to " ++ Id.print id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") + end) in try (** FIXME: should be moved to taccoerce *) @@ -1061,18 +1040,17 @@ let interp_destruction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } + | Some c -> keep,ElimOnConstr (fun env sigma -> (sigma, (c,NoBindings))) with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in - let f = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in + let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in - Sigma.Unsafe.of_pair ((c,NoBindings), sigma) - } in + (sigma, (c,NoBindings)) + in keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and @@ -1110,17 +1088,17 @@ let read_pattern lfun ist env sigma = function let cons_and_check_name id l = if Id.List.mem id l then user_err ~hdr:"read_match_goal_hyps" ( - str "Hypothesis pattern-matching variable " ++ pr_id id ++ + str "Hypothesis pattern-matching variable " ++ Id.print id ++ str " used twice in the same pattern.") else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | [] -> [] @@ -1208,9 +1186,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) end | TacAbstract (tac,ido) -> - Proofview.Goal.enter { enter = begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist tac) - end } + end | TacThen (t1,t) -> Tacticals.New.tclTHEN (interp_tactic ist t1) (interp_tactic ist t) | TacDispatch tl -> @@ -1328,12 +1306,13 @@ and interp_tacarg ist arg : Val.t Ftactic.t = | TacGeneric arg -> interp_genarg ist arg | Reference r -> interp_ltac_reference false ist r | ConstrMayEval c -> - Ftactic.s_enter { s_enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in - Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return (Value.of_constr c_interp)) + end | TacCall (loc,(r,[])) -> interp_ltac_reference true ist r | TacCall (loc,(f,l)) -> @@ -1342,18 +1321,19 @@ and interp_tacarg ist arg : Val.t Ftactic.t = Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs -> interp_app loc ist fv largs | TacFreshId l -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let id = interp_fresh_id ist (pf_env gl) (project gl) l in Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id))) - end } + end | TacPretype c -> - Ftactic.s_enter { s_enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in - let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in - Sigma (Ftactic.return (Value.of_constr c), sigma, p) - end } + let c = interp_uconstr ist env sigma c in + let (sigma, c) = type_uconstr ist c env sigma in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return (Value.of_constr c)) + end | TacNumgoals -> Ftactic.lift begin let open Proofview.Notations in @@ -1423,7 +1403,7 @@ and tactic_of_value ist vle = (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum pr_name vars ++ Pp.str ".") + pr_enum Name.print vars ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in @@ -1514,16 +1494,16 @@ and interp_match ist lz constr lmr = Proofview.tclZERO ~info e end end >>= fun constr -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr) - end } + end (* Interprets the Match Context expressions *) and interp_match_goal ist lz lr lmr = - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let hyps = Proofview.Goal.hyps gl in @@ -1531,7 +1511,7 @@ and interp_match_goal ist lz lr lmr = let concl = Proofview.Goal.concl gl in let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr) - end } + end (* Interprets extended tactic generic arguments *) and interp_genarg ist x : Val.t Ftactic.t = @@ -1568,24 +1548,25 @@ and interp_genarg ist x : Val.t Ftactic.t = independently of goals. *) and interp_genarg_constr_list ist x = - Ftactic.nf_s_enter { s_enter = begin fun gl -> + Ftactic.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in let lc = in_list (val_tag wit_constr) lc in - Sigma.Unsafe.of_pair (Ftactic.return lc, sigma) - end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return lc) + end and interp_genarg_var_list ist x = - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in let lc = in_list (val_tag wit_var) lc in Ftactic.return lc - end } + end (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : EConstr.t Ftactic.t = @@ -1594,7 +1575,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = (val_interp ist e) begin function (err, info) -> match err with | Not_found -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in Proofview.tclLIFT begin debugging_step ist (fun () -> @@ -1602,11 +1583,11 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = Pptactic.pr_glob_tactic env e) end <*> Proofview.tclZERO Not_found - end } + end | err -> Proofview.tclZERO ~info err end end >>= fun result -> - Ftactic.enter { enter = begin fun gl -> + Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let result = Value.normalize result in @@ -1623,7 +1604,7 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = let env = Proofview.Goal.env gl in Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ str "offending expression: " ++ fnl() ++ pr_inspect env e result) - end } + end (* Interprets tactic expressions : returns a "tactic" *) @@ -1645,7 +1626,7 @@ and interp_atomic ist tac : unit Proofview.tactic = match tac with (* Basic tactics *) | TacIntroPattern (ev,l) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in @@ -1655,11 +1636,11 @@ and interp_atomic ist tac : unit Proofview.tactic = (* spiwack: print uninterpreted, not sure if it is the expected behaviour. *) (Tactics.intro_patterns ev l')) sigma - end } + end | TacApply (a,ev,cb,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let l = List.map (fun (k,c) -> @@ -1672,10 +1653,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma,(id,cl) = interp_in_hyp_as ist env sigma cl in sigma, Tactics.apply_delayed_in a ev id l cl in Tacticals.New.tclWITHHOLES ev tac sigma - end } + end end | TacElim (ev,(keep,cb),cbo) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in @@ -1685,9 +1666,9 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end } + end | TacCase (ev,(keep,cb)) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in @@ -1696,11 +1677,11 @@ and interp_atomic ist tac : unit Proofview.tactic = name_atomic ~env (TacCase(ev,(keep,cb))) tac in Tacticals.New.tclWITHHOLES ev named_tac sigma - end } + end | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1708,14 +1689,14 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) + end end | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in @@ -1723,26 +1704,29 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in - Sigma.Unsafe.of_pair (tac, sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0) end - | TacAssert (b,t,ipat,c) -> - Proofview.Goal.enter { enter = begin fun gl -> + end + | TacAssert (ev,b,t,ipat,c) -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let (sigma,c) = - (if Option.is_empty t then interp_constr else interp_type) ist env sigma c + let (sigma,c) = + let expected_type = + if Option.is_empty t then WithoutTypeConstraint else IsType in + let flags = open_constr_use_classes_flags () in + interp_open_constr ~expected_type ~flags ist env sigma c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (Option.map (interp_tactic ist)) t in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacAssert(b,Option.map (Option.map ignore) t,ipat,c)) + (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c)) (Tactics.forward b tac ipat' c)) sigma - end } + end | TacGeneralize cl -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in @@ -1750,46 +1734,47 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacGeneralize cl) (Tactics.generalize_gen cl)) sigma - end } - | TacLetTac (na,c,clp,b,eqpat) -> - Proofview.Goal.enter { enter = begin fun gl -> + end + | TacLetTac (ev,na,c,clp,b,eqpat) -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let clp = interp_clause ist env sigma clp in let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in - if Locusops.is_nowhere clp then + if Locusops.is_nowhere clp (* typically "pose" *) then (* We try to fully-typecheck the term *) - let (sigma,c_interp) = interp_constr ist env sigma c in + let flags = open_constr_use_classes_flags () in + let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in let let_tac b na c cl eqpat = let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in Tactics.letin_tac with_eq na c None cl in let na = interp_name ist env sigma na in - Tacticals.New.tclWITHHOLES false + Tacticals.New.tclWITHHOLES ev (name_atomic ~env - (TacLetTac(na,c_interp,clp,b,eqpat)) + (TacLetTac(ev,na,c_interp,clp,b,eqpat)) (let_tac b na c_interp clp eqpat)) sigma else (* We try to keep the pattern structure as much as possible *) let let_pat_tac b na c cl eqpat = let id = Option.default (Loc.tag IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in - Tactics.letin_pat_tac with_eq na c cl + Tactics.letin_pat_tac ev with_eq na c cl in let (sigma',c) = interp_pure_open_constr ist env sigma c in name_atomic ~env - (TacLetTac(na,c,clp,b,eqpat)) - (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) + (TacLetTac(ev,na,c,clp,b,eqpat)) + (Tacticals.New.tclWITHHOLES ev (let_pat_tac b (interp_name ist env sigma na) (sigma,c) clp eqpat) sigma') - end } + end (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let sigma,l = @@ -1808,23 +1793,23 @@ and interp_atomic ist tac : unit Proofview.tactic = let l,lp = List.split l in let sigma,el = Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in - let tac = name_atomic ~env + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) - (Tactics.induction_destruct isrec ev (l,el)) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + (Tactics.induction_destruct isrec ev (l,el))) + end (* Conversion *) | TacReduce (r,cl) -> - Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in - Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma) - end } + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) + end | TacChange (None,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let is_onhyps = match cl.onhyps with | None | Some [] -> true | _ -> false @@ -1833,58 +1818,50 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars = { Sigma.run = begin fun sigma -> + let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in - let sigma = Sigma.to_evar_map sigma in let ist = { ist with lfun = lfun' } in - let (sigma, c) = if is_onhyps && is_onconcl then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c - in - Sigma.Unsafe.of_pair (c, sigma) - end } in + in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) - end } + end end | TacChange (Some op,c,cl) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in - let c_interp patvars = { Sigma.run = begin fun sigma -> + let c_interp patvars sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in try - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) + interp_constr ist env sigma c with e when to_catch e (* Hack *) -> user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") - end } in + in Tactics.change (Some op) c_interp (interp_clause ist env sigma cl) - end } + end end (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let l' = List.map (fun (b,m,(keep,c)) -> - let f = { delayed = fun env sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in - Sigma.Unsafe.of_pair (c, sigma) - } in + let f env sigma = + interp_open_constr_with_bindings ist env sigma c + in (b,m,keep,f)) l in let env = Proofview.Goal.env gl in let sigma = project gl in @@ -1895,9 +1872,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by), Equality.Naive) by)) - end } + end | TacInversion (DepInversion (k,c,ids),hyp) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = @@ -1913,9 +1890,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion(DepInversion(k,c_interp,ids),dqhyps)) (Inv.dinv k c_interp ids_interp dqhyps)) sigma - end } + end | TacInversion (NonDepInversion (k,idl,ids),hyp) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let hyps = interp_hyp_list ist env sigma idl in @@ -1925,20 +1902,19 @@ and interp_atomic ist tac : unit Proofview.tactic = (name_atomic ~env (TacInversion (NonDepInversion (k,hyps,ids),dqhyps)) (Inv.inv_clause k ids_interp hyps dqhyps)) sigma - end } + end | TacInversion (InversionUsing (c,idl),hyp) -> - Proofview.Goal.s_enter { s_enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = interp_constr ist env sigma c in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in - let tac = name_atomic ~env + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (name_atomic ~env (TacInversion (InversionUsing (c_interp,hyps),dqhyps)) - (Leminv.lemInv_clause dqhyps c_interp hyps) - in - Sigma.Unsafe.of_pair (tac, sigma) - end } + (Leminv.lemInv_clause dqhyps c_interp hyps)) + end (* Initial call for interpretation *) @@ -1959,7 +1935,7 @@ let eval_tactic_ist ist t = let interp_tac_gen lfun avoid_ids debug t = - Proofview.Goal.enter { enter = begin fun gl -> + 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 @@ -1967,7 +1943,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) - end } + end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -1986,9 +1962,9 @@ let hide_interp global t ot = Proofview.tclENV >>= fun env -> hide_interp env else - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> hide_interp (Proofview.Goal.env gl) - end } + end (***************************************************************************) (** Register standard arguments *) @@ -2021,37 +1997,35 @@ let () = let () = declare_uniform wit_string -let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl -> +let lift f = (); fun ist x -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in Ftactic.return (f ist env sigma x) -end } +end -let lifts f = (); fun ist x -> Ftactic.nf_s_enter { s_enter = begin fun gl -> +let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl -> let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in + let sigma = Proofview.Goal.sigma gl in let (sigma, v) = f ist env sigma x in - Sigma.Unsafe.of_pair (Ftactic.return v, sigma) -end } + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (Ftactic.return v) +end -let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma -> - let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in - Sigma.Unsafe.of_pair (bl, sigma) - } +let interp_bindings' ist bl = Ftactic.return begin fun env sigma -> + interp_bindings ist env sigma bl + end -let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> - let (sigma, c) = interp_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in - Sigma.Unsafe.of_pair (c, sigma) - } +let interp_constr_with_bindings' ist c = Ftactic.return begin fun env sigma -> + interp_constr_with_bindings ist env sigma c + end -let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> - let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in - Sigma.Unsafe.of_pair (c, sigma) - } +let interp_open_constr_with_bindings' ist c = Ftactic.return begin fun env sigma -> + interp_open_constr_with_bindings ist env sigma c + end -let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl -> +let interp_destruction_arg' ist c = Ftactic.enter begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) -end } +end let interp_pre_ident ist env sigma s = s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string @@ -2084,9 +2058,9 @@ let () = register_interp0 wit_ltac interp let () = - register_interp0 wit_uconstr (fun ist c -> Ftactic.enter { enter = begin fun gl -> + register_interp0 wit_uconstr (fun ist c -> Ftactic.enter begin fun gl -> Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c) - end }) + end) (***************************************************************************) (* Other entry points *) @@ -2117,7 +2091,7 @@ let _ = let dummy_id = Id.of_string "_" let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter { enter = begin fun gl -> + let tac _ ist = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in let map = function @@ -2130,7 +2104,7 @@ let lift_constr_tac_to_ml_tac vars tac = in let args = List.map_filter map vars in tac args ist - end } in + end in tac let vernac_debug b = diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 2ec45312e..a1841afe3 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Tactic_debug open EConstr @@ -72,11 +73,27 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> Id.t Loc.located -> Id.t +val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> + ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> + Glob_term.closed_glob_constr + +val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Glob_term.closed_glob_constr + val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr bindings -> Evd.evar_map * constr bindings + glob_constr_and_expr bindings -> Evd.evar_map * constr bindings + +val interp_open_constr : ?expected_type:Pretyping.typing_constraint -> + ?flags:Pretyping.inference_flags -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr + +val interp_open_constr_with_classes : ?expected_type:Pretyping.typing_constraint -> + interp_sign -> Environ.env -> Evd.evar_map -> + glob_constr_and_expr -> Evd.evar_map * EConstr.constr val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr with_bindings -> Evd.evar_map * EConstr.constr with_bindings diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4390ff08b..6d33724f1 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API +open Grammar_API open Util open Tacexpr open Mod_subst @@ -14,7 +16,6 @@ open Stdarg open Tacarg open Misctypes open Globnames -open Term open Genredexpr open Patternops @@ -91,7 +92,7 @@ open Printer let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in - if not (eq_constr (Universes.constr_of_global ref') t') then + if not (is_global ref' t') then Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; @@ -146,13 +147,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) - | TacAssert (b,otac,na,c) -> - TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na, + | TacAssert (ev,b,otac,na,c) -> + TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na, subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacLetTac (id,c,clp,b,eqpat) -> - TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) + | TacLetTac (ev,id,c,clp,b,eqpat) -> + TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat) (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index c1bf27257..2cfe8fac9 100644 --- a/plugins/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Tacexpr open Mod_subst open Genarg diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 294cba4d7..b909c930d 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -6,14 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Util open Names open Pp open Tacexpr open Termops -open Nameops -open Proofview.Notations - let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -57,10 +55,10 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end } + end (* Prints the commands *) @@ -259,14 +257,14 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function | Anonymous -> str " (unbound)" - | Name id -> str " (bound to " ++ pr_id id ++ str ")" + | Name id -> str " (bound to " ++ Id.print id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env sigma (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ str " has been matched: " ++ print_constr_env env sigma c) else return () @@ -361,7 +359,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacMLCall t -> quote (Pptactic.pr_glob_tactic (Global.env()) t) | Tacexpr.LtacVarCall (id,t) -> - quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ + quote (Id.print id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) @@ -372,7 +370,7 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index ac35464c4..6cfaed305 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Environ open Pattern open Names diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 5b5cd06cc..6dcef414c 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -9,6 +9,7 @@ (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) +open API open Names open Tacexpr open Context.Named.Declaration diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 300b546f1..304eec463 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API + (** This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal. *) diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index a5ba3b837..53dfe22a9 100644 --- a/plugins/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Libobject open Pp diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index ed759a76d..2817b54a1 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Tacexpr open Vernacexpr diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4ec111e01..5eacb1a95 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Term open EConstr open Hipattern @@ -196,7 +197,7 @@ let flatten_contravariant_disj _ ist = let make_unfold name = let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in - let const = Constant.make2 (MPfile dir) (Label.make name) in + let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) let u_iff = make_unfold "iff" @@ -220,9 +221,7 @@ let apply_nnpp _ ist = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> try - let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in - let nnpp = EConstr.of_constr nnpp in - apply nnpp + Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply with Not_found -> tclFAIL 0 (Pp.mt ()) end diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget deleted file mode 100644 index a28fb770b..000000000 --- a/plugins/ltac/vo.itarget +++ /dev/null @@ -1 +0,0 @@ -Ltac.vo |