aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml415
-rw-r--r--plugins/ltac/g_tactic.ml448
-rw-r--r--plugins/ltac/pptactic.ml74
-rw-r--r--plugins/ltac/pptactic.mli4
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/rewrite.ml41
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml14
-rw-r--r--plugins/ltac/tacinterp.ml102
-rw-r--r--plugins/ltac/tacinterp.mli18
-rw-r--r--plugins/ltac/tacsubst.ml11
-rw-r--r--plugins/ltac/tauto.ml4
14 files changed, 166 insertions, 177 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b4..9726a5b401 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -306,7 +306,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
@@ -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
@@ -735,7 +736,6 @@ let rewrite_except h =
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")
@@ -747,8 +747,9 @@ let refl_equal =
let mkCaseEq a : unit Proofview.tactic =
Proofview.Goal.enter { 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|]))];
+ 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 { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1404b1c1f1..83bfd0233a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -538,38 +538,64 @@ 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 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 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)])
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2ba..9029858279 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -161,28 +161,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 +168,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
@@ -367,30 +345,6 @@ type 'a extra_genarg_printer =
| 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
@@ -571,7 +525,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 +536,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 +722,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 +740,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 ++
@@ -1280,9 +1234,9 @@ 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 (fst (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))
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 19bdf2d49f..4265c416b6 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -106,10 +106,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 3ff7b53c7e..b237e917d5 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -113,7 +113,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 +125,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
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 966b11d0e7..f028abde9a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -236,7 +236,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) ->
@@ -751,17 +751,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, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map evars) gr
+ in (Sigma.to_evar_map 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 +833,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 +854,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 +876,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)
}
@@ -1231,9 +1238,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
@@ -1419,7 +1424,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
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 75f89a81e1..f44ccbd3b5 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -502,7 +502,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/tacenv.ml b/plugins/ltac/tacenv.ml
index e3c2b4ad51..efb7e780db 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -24,7 +24,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/tacexpr.mli b/plugins/ltac/tacexpr.mli
index bf760e7bba..b78dc37426 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -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 e431a13bc2..d201cf9490 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -189,7 +189,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 +198,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 +489,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 +718,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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d11..37fdd185e9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -379,7 +379,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)
@@ -577,57 +577,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 +662,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
@@ -1116,11 +1106,11 @@ let cons_and_check_name 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)
| [] -> []
@@ -1423,7 +1413,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
@@ -1727,18 +1717,21 @@ and interp_atomic ist tac : unit Proofview.tactic =
Sigma.Unsafe.of_pair (tac, sigma)
end }
end
- | TacAssert (b,t,ipat,c) ->
+ | TacAssert (ev,b,t,ipat,c) ->
Proofview.Goal.enter { 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 }
| TacGeneralize cl ->
@@ -1751,36 +1744,37 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacGeneralize cl)
(Tactics.generalize_gen cl)) sigma
end }
- | TacLetTac (na,c,clp,b,eqpat) ->
+ | TacLetTac (ev,na,c,clp,b,eqpat) ->
Proofview.Goal.enter { 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 }
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 2ec45312ea..fb50a64346 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -72,11 +72,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 4390ff08b4..2858df3130 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,6 @@ open Stdarg
open Tacarg
open Misctypes
open Globnames
-open Term
open Genredexpr
open Patternops
@@ -91,7 +90,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 +145,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/tauto.ml b/plugins/ltac/tauto.ml
index 4ec111e014..d8e21d81d1 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -220,9 +220,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 20:25:29 +0000