aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml9
-rw-r--r--plugins/funind/functional_principles_proofs.ml38
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/indfun.ml8
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/merge.ml14
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/ltac/extratactics.ml49
-rw-r--r--plugins/ltac/pptactic.ml2
-rw-r--r--plugins/ltac/rewrite.ml37
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacintern.ml2
-rw-r--r--plugins/ltac/tacinterp.ml6
-rw-r--r--plugins/ltac/tacsubst.ml3
-rw-r--r--plugins/ltac/tauto.ml4
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--plugins/quote/quote.ml71
17 files changed, 117 insertions, 110 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b3017f359b..43c06a54d4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -231,9 +231,9 @@ let make_prb gls depth additionnal_terms =
let build_projection intype (cstr:pconstructor) special default gls=
let open Tacmach.New in
let ci= (snd(fst cstr)) in
- let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+ let sigma, body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
let id=pf_get_new_id (Id.of_string "t") gls in
- mkLambda(Name id,intype,body)
+ sigma, mkLambda(Name id,intype,body)
(* generate an adhoc tactic following the proof tree *)
@@ -346,12 +346,13 @@ let rec proof_tac p : unit Proofview.tactic =
let special=mkRel (1+nargs-argind) in
refresh_universes (type_of ti) (fun intype ->
refresh_universes (type_of default) (fun outtype ->
- let proj =
+ let sigma, proj =
build_projection intype cstr special default gl
in
let injt=
app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
- Tacticals.New.tclTHEN injt (proof_tac prf)))
+ Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ (Tacticals.New.tclTHEN injt (proof_tac prf))))
with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end }
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 434fb14a6e..0041797de7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -944,7 +944,7 @@ let generalize_non_dep hyp g =
((* observe_tac "thin" *) (thin to_revert))
g
-let id_of_decl = RelDecl.get_name %> Nameops.out_name
+let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id
let var_of_decl = id_of_decl %> mkVar
let revert idl =
tclTHEN
@@ -1127,11 +1127,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
)
in
observe (str "full_params := " ++
- prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
full_params
);
observe (str "princ_params := " ++
- prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id)
+ prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id)
princ_params
);
observe (str "fbody_with_full_params := " ++
@@ -1158,7 +1158,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(fun i types ->
let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in
{ idx = idxs.(i) - fix_offset;
- name = Nameops.out_name (fresh_id names.(i));
+ name = Nameops.Name.get_id (fresh_id names.(i));
types = types;
offset = fix_offset;
nb_realargs =
@@ -1181,7 +1181,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in
let app_f = mkApp(f,first_args) in
let pte_args = (Array.to_list first_args)@[app_f] in
- let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in
+ let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
@@ -1208,9 +1208,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
num_in_block = num
}
in
-(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *)
+(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *)
(* str " to " ++ Ppconstr.pr_id info.name); *)
- (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
+ (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info)
)
0
(Id.Map.empty,[])
@@ -1284,7 +1284,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(do_replace evd
full_params
(fix_info.idx + List.length princ_params)
- (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params))
+ (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params))
(all_funs.(fix_info.num_in_block))
fix_info.num_in_block
all_funs
@@ -1563,17 +1563,17 @@ let prove_principle_for_gen
| _ -> assert false
in
(* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *)
- let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in
+ let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in
let relation = substl subst_constrs relation in
let input_type = substl subst_constrs rec_arg_type in
- let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
+ let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in
let acc_rec_arg_id =
- Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
+ Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
in
- let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
+ let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
((* observe_tac "prove_rec_arg_acc" *)
(tclCOMPLETE
@@ -1591,7 +1591,7 @@ let prove_principle_for_gen
)
g
in
- let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
+ let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in
let lemma =
match !tcc_lemma_ref with
| Undefined -> user_err Pp.(str "No tcc proof !!")
@@ -1639,7 +1639,7 @@ let prove_principle_for_gen
[
observe_tac "start_tac" start_tac;
h_intros
- (List.rev_map (get_name %> Nameops.out_name)
+ (List.rev_map (get_name %> Nameops.Name.get_id)
(princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
);
(* observe_tac "" *) Proofview.V82.of_tactic (assert_by
@@ -1677,14 +1677,14 @@ let prove_principle_for_gen
in
let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in
let predicates_names =
- List.map (get_name %> Nameops.out_name) princ_info.predicates
+ List.map (get_name %> Nameops.Name.get_id) princ_info.predicates
in
let pte_info =
{ proving_tac =
(fun eqs ->
(* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *)
-(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *)
-(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *)
+(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *)
+(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *)
(* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *)
(* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *)
@@ -1693,7 +1693,7 @@ let prove_principle_for_gen
is_mes acc_inv fix_id
(!tcc_list@(List.map
- (get_name %> Nameops.out_name)
+ (get_name %> Nameops.Name.get_id)
(princ_info.args@princ_info.params)
)@ ([acc_rec_arg_id])) eqs
)
@@ -1722,7 +1722,7 @@ let prove_principle_for_gen
(* observe_tac "instanciate_hyps_with_args" *)
(instanciate_hyps_with_args
make_proof
- (List.map (get_name %> Nameops.out_name) princ_info.branches)
+ (List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
(List.rev args_ids)
)
gl'
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 18d63dd94b..9425271671 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
then List.tl args
else args
in
- Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl),
+ Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl),
Term.compose_prod real_args (mkSort new_sort))
in
let new_predicates =
@@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
with
| Toberemoved ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
@@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
with
| Toberemoved ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in
new_b, List.map pop binders_to_remove_from_b
| Toberemoved_with_rel (n,c) ->
-(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *)
let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in
new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
end
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 74c0eb4cc7..4946285e16 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -200,13 +200,13 @@ let is_rec names =
| GIf(b,_,lhs,rhs) ->
(lookup names b) || (lookup names lhs) || (lookup names rhs)
| GProd(na,_,t,b) | GLambda(na,_,t,b) ->
- lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
+ lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b
| GLetIn(na,b,t,c) ->
- lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c
+ lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c
| GLetTuple(nal,_,t,b) -> lookup names t ||
lookup
(List.fold_left
- (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
+ (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc)
names
nal
)
@@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) =
| Constrexpr.CLocalAssum (nal,_,_) ->
List.map
(fun (loc,n) -> CAst.make ?loc @@
- CRef(Libnames.Ident(loc, Nameops.out_name n),None))
+ CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
nal
| Constrexpr.CLocalPattern _ -> assert false
)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d68bdc2153..12232dd83d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -421,7 +421,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let params_bindings,avoid =
List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
p::bindings,id::avoid
)
([],pf_ids_of_hyps g)
@@ -431,7 +431,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let lemmas_bindings =
List.rev (fst (List.fold_left2
(fun (bindings,avoid) decl p ->
- let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
+ let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in
(nf_zeta p)::bindings,id::avoid)
([],avoid)
princ_infos.predicates
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b2c8489ce1..7634437171 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -133,20 +133,6 @@ let prNamedRLDecl s lc =
prstr "\n";
end
-let showind (id:Id.t) =
- let cstrid = Constrintern.global_reference id in
- let (ind1, u),cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
- let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
- let u = EConstr.Unsafe.to_instance u in
- List.iter (fun decl ->
- print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
- prconstr (RelDecl.get_type decl); print_string "\n")
- ib1.mind_arity_ctxt;
- Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) (ind1, u));
- Array.iteri
- (fun i x -> Printf.printf"type constr %d :" i ; prconstr x)
- ib1.mind_user_lc
-
(** {2 Misc} *)
exception Found of int
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2f9f708768..62eba9513d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -879,7 +879,7 @@ let rec make_rewrite_list expr_info max = function
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
let def_na,_,_ = destProd sigma t in
- Nameops.out_name k_na,Nameops.out_name def_na
+ Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
in
Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
true (* dep proofs also: *) true
@@ -905,7 +905,7 @@ let make_rewrite expr_info l hp max =
let k_na,_,t = destProd sigma t_eq in
let _,_,t = destProd sigma t in
let def_na,_,_ = destProd sigma t in
- Nameops.out_name k_na,Nameops.out_name def_na
+ Nameops.Name.get_id k_na,Nameops.Name.get_id def_na
in
observe_tac (str "general_rewrite_bindings")
(Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cba9c13648..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
@@ -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/pptactic.ml b/plugins/ltac/pptactic.ml
index 4e254ea766..580c21d40e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -571,7 +571,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 ++
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 966b11d0e7..dadcfb9f26 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -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
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/tacintern.ml b/plugins/ltac/tacintern.ml
index 2dc3bb3786..0096abfa69 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -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 6b0914ff95..594c4fa15f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1113,11 +1113,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)
| [] -> []
@@ -1420,7 +1420,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
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index f5e6f05cee..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') ;
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
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index ee748567b8..d7408e88ec 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -39,10 +39,10 @@ open OmegaSolver
let elim_id id =
Proofview.Goal.enter { enter = begin fun gl ->
- simplest_elim (Tacmach.New.pf_global id gl)
+ simplest_elim (mkVar id)
end }
let resolve_id id = Proofview.Goal.enter { enter = begin fun gl ->
- apply (Tacmach.New.pf_global id gl)
+ apply (mkVar id)
end }
let timing timer_name f arg = f arg
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 7412de1e80..ba8356b525 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -456,39 +456,56 @@ let quote_terms env sigma ivs lc =
term. Ring for example needs that, but Ring doesn't use Quote
yet. *)
+let pf_constrs_of_globals l =
+ let rec aux l acc =
+ match l with
+ [] -> Proofview.tclUNIT (List.rev acc)
+ | hd :: tl ->
+ Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc)
+ in aux l []
+
let quote f lid =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let f = Tacmach.New.pf_global f gl in
- let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
- let ivs = compute_ivs f cl gl in
- let concl = Proofview.Goal.concl gl in
- let quoted_terms = quote_terms env sigma ivs [concl] in
- let (p, vm) = match quoted_terms with
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let fg = Tacmach.New.pf_global f gl in
+ let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+ Tacticals.New.pf_constr_of_global fg >>= fun f ->
+ pf_constrs_of_globals clg >>= fun cl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in
+ let concl = Proofview.Goal.concl gl in
+ let quoted_terms = quote_terms env sigma ivs [concl] in
+ let (p, vm) = match quoted_terms with
| [p], vm -> (p,vm)
| _ -> assert false
- in
- match ivs.variable_lhs with
- | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
- | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+ in
+ match ivs.variable_lhs with
+ | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
+ | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+ end }
end }
let gen_quote cont c f lid =
- Proofview.Goal.nf_enter { enter = begin fun gl ->
- let env = Proofview.Goal.env gl in
- let sigma = Tacmach.New.project gl in
- let f = Tacmach.New.pf_global f gl in
- let cl = List.map (fun id -> EConstr.to_constr sigma (Tacmach.New.pf_global id gl)) lid in
- let ivs = compute_ivs f cl gl in
- let quoted_terms = quote_terms env sigma ivs [c] in
- let (p, vm) = match quoted_terms with
- | [p], vm -> (p,vm)
- | _ -> assert false
- in
- match ivs.variable_lhs with
- | None -> cont (mkApp (f, [| p |]))
- | Some _ -> cont (mkApp (f, [| vm; p |]))
+ Proofview.Goal.enter { enter = begin fun gl ->
+ let fg = Tacmach.New.pf_global f gl in
+ let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
+ Tacticals.New.pf_constr_of_global fg >>= fun f ->
+ pf_constrs_of_globals clg >>= fun cl ->
+ Proofview.Goal.nf_enter { enter = begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let cl = List.map (EConstr.to_constr sigma) cl in
+ let ivs = compute_ivs f cl gl in
+ let quoted_terms = quote_terms env sigma ivs [c] in
+ let (p, vm) = match quoted_terms with
+ | [p], vm -> (p,vm)
+ | _ -> assert false
+ in
+ match ivs.variable_lhs with
+ | None -> cont (mkApp (f, [| p |]))
+ | Some _ -> cont (mkApp (f, [| vm; p |]))
+ end }
end }
(*i
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 23:28:21 +0000