diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/dune | 6 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/term_dnet.ml | 2 |
6 files changed, 14 insertions, 8 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index aca7f6c65e..bfee0422e7 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -28,7 +28,7 @@ type term_label = | SortLabel let compare_term_label t1 t2 = match t1, t2 with -| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 +| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2 | _ -> Pervasives.compare t1 t2 (** OK *) type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything diff --git a/tactics/dune b/tactics/dune new file mode 100644 index 0000000000..908dde5253 --- /dev/null +++ b/tactics/dune @@ -0,0 +1,6 @@ +(library + (name tactics) + (synopsis "Coq's Core Tactics [ML implementation]") + (public_name coq.tactics) + (wrapped false) + (libraries printing)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 43a450ea71..dce1a1bef6 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -288,7 +288,7 @@ let lookup_tacs sigma concl st se = let sl' = List.stable_sort pri_order_int l' in List.merge pri_order_int se.sentry_nopat sl' -module Constr_map = Map.Make(RefOrdered) +module Constr_map = Map.Make(GlobRef.Ordered) let is_transparent_gr (ids, csts) = function | VarRef id -> Id.Pred.mem id ids diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 21520f5d2b..e4013152e6 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -154,7 +154,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.add_private + const, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -174,7 +174,7 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Safe_typing.add_private + Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -187,7 +187,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.add_private + s, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind, s]) Safe_typing.empty_private_constants diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2a8ebe08ca..d536204ec3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -125,7 +125,7 @@ let unsafe_intro env store decl b = let ninst = mkRel 1 :: inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in - (sigma, mkNamedLambda_or_LetIn decl ev) + (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev) end let introduction id = @@ -5007,7 +5007,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in - let effs = add_private eff + let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 8bdcc63215..03d2a17eee 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -100,7 +100,7 @@ struct | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 | DSort, _ -> -1 | _, DSort -> 1 - | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 + | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2 | DRef _, _ -> -1 | _, DRef _ -> 1 | DCtx (tl1, tr1), DCtx (tl2, tr2) |