aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml11
-rw-r--r--plugins/extraction/extract_env.ml8
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/table.ml26
-rw-r--r--plugins/extraction/table.mli2
-rw-r--r--plugins/funind/functional_principles_types.ml30
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun_common.ml31
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--plugins/ltac/tacexpr.ml35
-rw-r--r--plugins/ltac/tacexpr.mli35
-rw-r--r--plugins/ltac/tacinterp.ml15
-rw-r--r--plugins/omega/g_omega.mlg2
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/syntax/ascii_syntax.ml5
-rw-r--r--plugins/syntax/r_syntax.ml14
-rw-r--r--plugins/syntax/string_syntax.ml3
19 files changed, 72 insertions, 167 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index f235bb8986..bdeb6fca60 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -112,17 +112,12 @@ let pseudo_qualify = qualify "__"
let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
-[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-let uncapitalize = String.uncapitalize
-[@@@ocaml.warning "+3"]
-
-let lowercase_id id = Id.of_string (uncapitalize (ascii_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize_ascii (ascii_of_id id))
let uppercase_id id =
let s = ascii_of_id id in
assert (not (String.is_empty s));
if s.[0] == '_' then Id.of_string ("Coq_"^s)
- else Id.of_string (capitalize s)
+ else Id.of_string (String.capitalize_ascii s)
type kind = Term | Type | Cons | Mod
@@ -593,7 +588,7 @@ let pp_global k r =
let ls = ref_renaming (k,r) in
assert (List.length ls > 1);
let s = List.hd ls in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
if ModPath.equal mp (top_visible_mp ()) then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5d3115d8d7..b0f6301192 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -30,7 +30,7 @@ open Common
let toplevel_env () =
let get_reference = function
| (_,kn), Lib.Leaf o ->
- let mp,_,l = KerName.repr kn in
+ let mp,l = KerName.repr kn in
begin match Libobject.object_tag o with
| "CONSTANT" ->
let constant = Global.lookup_constant (Constant.make1 kn) in
@@ -124,7 +124,7 @@ module Visit : VISIT = struct
end
let add_field_label mp = function
- | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make2 mp lab)
+ | (lab, (SFBconst _|SFBmind _)) -> Visit.add_kn (KerName.make mp lab)
| (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
let rec add_labels mp = function
@@ -208,10 +208,10 @@ let env_for_mtb_with_def env mp me reso idl =
Modops.add_structure mp before reso env
let make_cst resolver mp l =
- Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.constant_of_delta_kn resolver (KerName.make mp l)
let make_mind resolver mp l =
- Mod_subst.mind_of_delta_kn resolver (KerName.make2 mp l)
+ Mod_subst.mind_of_delta_kn resolver (KerName.make mp l)
(* From a [structure_body] (i.e. a list of [structure_field_body])
to specifications. *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index e6234c1452..97fe9f24d5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,10 +21,8 @@ open Mlutil
open Common
(*s Haskell renaming issues. *)
-[@@@ocaml.warning "-3"] (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
-let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
-let pr_upper_id id = str (String.capitalize (Id.to_string id))
-[@@@ocaml.warning "+3"]
+let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
+let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e05e82af6f..7b4fd280bd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -22,11 +22,6 @@ open Util
open Pp
open Miniml
-[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *)
-let capitalize = String.capitalize
-[@@@ocaml.warning "+3"]
-
-
(** Sets and maps for [global_reference] that use the "user" [kernel_name]
instead of the canonical one *)
@@ -41,16 +36,16 @@ let occur_kn_in_ref kn = function
| ConstRef _ | VarRef _ -> false
let repr_of_r = function
- | ConstRef kn -> Constant.repr3 kn
+ | ConstRef kn -> Constant.repr2 kn
| IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+ | ConstructRef ((kn,_),_) -> MutInd.repr2 kn
| VarRef v -> KerName.repr (Lib.make_kn v)
let modpath_of_r r =
- let mp,_,_ = repr_of_r r in mp
+ let mp,_ = repr_of_r r in mp
let label_of_r r =
- let _,_,l = repr_of_r r in l
+ let _,l = repr_of_r r in l
let rec base_mp = function
| MPdot (mp,l) -> base_mp mp
@@ -61,7 +56,7 @@ let is_modfile = function
| _ -> false
let raw_string_of_modfile = function
- | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f)))
+ | MPfile f -> String.capitalize_ascii (Id.to_string (List.hd (DirPath.repr f)))
| _ -> assert false
let is_toplevel mp =
@@ -100,7 +95,7 @@ let rec parse_labels2 ll mp1 = function
let labels_of_ref r =
let mp_top = Lib.current_mp () in
- let mp,_,l = repr_of_r r in
+ let mp,l = repr_of_r r in
parse_labels2 [l] mp_top mp
@@ -194,7 +189,7 @@ let init_recursors () = recursors := KNset.empty
let add_recursors env ind =
let kn = MutInd.canonical ind in
let mk_kn id =
- KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
+ KerName.make (KerName.modpath kn) (Label.of_id id)
in
let mib = Environ.lookup_mind ind env in
Array.iter
@@ -292,7 +287,7 @@ let safe_pr_long_global r =
try Printer.pr_global r
with Not_found -> match r with
| ConstRef kn ->
- let mp,_,l = Constant.repr3 kn in
+ let mp,l = Constant.repr2 kn in
str ((ModPath.to_string mp)^"."^(Label.to_string l))
| _ -> assert false
@@ -658,8 +653,7 @@ let inline_extraction : bool * GlobRef.t list -> obj =
cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
classify_function = (fun o -> Substitute o);
- discharge_function =
- (fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
+ discharge_function = (fun (_,x) -> Some x);
subst_function =
(fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
}
@@ -784,7 +778,7 @@ let file_of_modfile mp =
let add_blacklist_entries l =
blacklist_table :=
- List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s)))
+ List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize_ascii s)))
l !blacklist_table
(* Registration of operations for rollback. *)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a8baeaf1b6..acc1bfee8a 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
(*s utilities about [module_path] and [kernel_names] and [GlobRef.t] *)
val occur_kn_in_ref : MutInd.t -> GlobRef.t -> bool
-val repr_of_r : GlobRef.t -> ModPath.t * DirPath.t * Label.t
+val repr_of_r : GlobRef.t -> ModPath.t * Label.t
val modpath_of_r : GlobRef.t -> ModPath.t
val label_of_r : GlobRef.t -> Label.t
val base_mp : ModPath.t -> ModPath.t
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b2a528a1fd..9ca91d62da 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,3 +1,13 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
open Printer
open CErrors
open Term
@@ -322,7 +332,8 @@ let generate_functional_principle (evd: Evd.evar_map ref)
try
let f = funs.(i) in
- let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
+ let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in
+ evd := sigma;
let new_sorts =
match sorts with
| None -> Array.make (Array.length funs) (type_sort)
@@ -394,7 +405,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
exception Not_Rec
-let get_funs_constant mp dp =
+let get_funs_constant mp =
let get_funs_constant const e : (Names.Constant.t*int) array =
match Constr.kind ((strip_lam e)) with
| Fix((_,(na,_,_))) ->
@@ -402,7 +413,7 @@ let get_funs_constant mp dp =
(fun i na ->
match na with
| Name id ->
- let const = Constant.make3 mp dp (Label.of_id id) in
+ let const = Constant.make2 mp (Label.of_id id) in
const,i
| Anonymous ->
anomaly (Pp.str "Anonymous fix.")
@@ -474,13 +485,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
- let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in
+ let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
let first_fun_kn =
try
fst (find_Function_infos (fst first_fun)).graph_ind
with Not_found -> raise No_graph_found
in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in
+ let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
@@ -507,8 +518,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
let i = ref (-1) in
let sorts =
List.rev_map (fun (_,x) ->
- Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
- )
+ let sigma, fs = Evd.fresh_sort_in_family !evd x in
+ evd := sigma; fs
+ )
fas
in
(* We create the first priciple by tactic *)
@@ -669,9 +681,9 @@ let build_case_scheme fa =
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_qualid f) in
let first_fun,u = destConst funs in
- let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
+ let funs_mp = Constant.modpath first_fun in
let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in
- let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
+ let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
let prop_sort = InProp in
let funs_indexes =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9eda19a86b..9a6169d42a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -898,11 +898,11 @@ let make_graph (f_ref : GlobRef.t) =
let id = Label.to_id (Constant.label c) in
[((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
in
- let mp,dp,_ = Constant.repr3 c in
+ let mp = Constant.modpath c in
do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list;
(* We register the infos *)
List.iter
- (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+ (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
expr_list)
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 4eee2c7a45..6ed382ca1c 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -297,36 +297,7 @@ let subst_Function (subst,finfos) =
let classify_Function infos = Libobject.Substitute infos
-let discharge_Function (_,finfos) =
- let function_constant' = Lib.discharge_con finfos.function_constant
- and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
- in
- if function_constant' == finfos.function_constant &&
- graph_ind' == finfos.graph_ind &&
- equation_lemma' == finfos.equation_lemma &&
- correctness_lemma' == finfos.correctness_lemma &&
- completeness_lemma' == finfos.completeness_lemma &&
- rect_lemma' == finfos.rect_lemma &&
- rec_lemma' == finfos.rec_lemma &&
- prop_lemma' == finfos.prop_lemma
- then Some finfos
- else
- Some { function_constant = function_constant' ;
- graph_ind = graph_ind' ;
- equation_lemma = equation_lemma' ;
- correctness_lemma = correctness_lemma' ;
- completeness_lemma = completeness_lemma';
- rect_lemma = rect_lemma';
- rec_lemma = rec_lemma';
- prop_lemma = prop_lemma' ;
- is_general = finfos.is_general
- }
+let discharge_Function (_,finfos) = Some finfos
let pr_ocst c =
let sigma, env = Pfedit.get_current_context () in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad11f853ca..56fe430077 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -450,7 +450,7 @@ let generalize_dependent_of x hyp g =
let tauto =
let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in
let mp = ModPath.MPfile (DirPath.make dp) in
- let kn = KerName.make2 mp (Label.make "tauto") in
+ let kn = KerName.make mp (Label.make "tauto") in
Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
let body = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic body
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7298342e1e..633d98a585 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -713,7 +713,7 @@ let mkDestructEq :
observe_tclTHENLIST (str "mkDestructEq")
[Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
- let changefun patvars sigma =
+ let changefun patvars env sigma =
pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 11d13d3a2f..8731cbf60d 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Goal_select.t =
- | SelectAlreadyFocused
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectNth of int
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectList of (int * int) list
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectId of Id.t
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectAll
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
-[@@ocaml.deprecated "Use [Goal_select.t]"]
-
-type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
- | ElimOnConstr of 'a
- [@ocaml.deprecated "Use constructors in [Tactics]"]
- | ElimOnIdent of lident
- [@ocaml.deprecated "Use constructors in [Tactics]"]
- | ElimOnAnonHyp of int
- [@ocaml.deprecated "Use constructors in [Tactics]"]
-[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
-
-type 'a destruction_arg =
- clear_flag * 'a Tactics.core_destruction_arg
-[@@ocaml.deprecated "Use Tactics.destruction_arg"]
-
-type inversion_kind = Inv.inversion_kind =
- | SimpleInversion
- [@ocaml.deprecated "Use constructors in [Inv]"]
- | FullInversion
- [@ocaml.deprecated "Use constructors in [Inv]"]
- | FullInversionClear
- [@ocaml.deprecated "Use constructors in [Inv]"]
-[@@ocaml.deprecated "Use Tactics.inversion_kind"]
-
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 6b131edaac..9958d6dcda 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Goal_select.t =
- | SelectAlreadyFocused
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectNth of int
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectList of (int * int) list
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectId of Id.t
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
- | SelectAll
- [@ocaml.deprecated "Use constructors in [Goal_select]"]
-[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
-
-type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
- | ElimOnConstr of 'a
- [@ocaml.deprecated "Use constructors in [Tactics]"]
- | ElimOnIdent of lident
- [@ocaml.deprecated "Use constructors in [Tactics]"]
- | ElimOnAnonHyp of int
- [@ocaml.deprecated "Use constructors in [Tactics]"]
-[@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
-
-type 'a destruction_arg =
- clear_flag * 'a Tactics.core_destruction_arg
-[@@ocaml.deprecated "Use Tactics.destruction_arg"]
-
-type inversion_kind = Inv.inversion_kind =
- | SimpleInversion
- [@ocaml.deprecated "Use constructors in [Inv]"]
- | FullInversion
- [@ocaml.deprecated "Use constructors in [Inv]"]
- | FullInversionClear
- [@ocaml.deprecated "Use constructors in [Inv]"]
-[@@ocaml.deprecated "Use Tactics.inversion_kind"]
-
type ('c,'d,'id) inversion_strength =
| NonDepInversion of
Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9f34df4608..f90e889678 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -283,6 +283,12 @@ let debugging_exception_step ist signal_anomaly e pp =
debugging_step ist (fun () ->
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
+let ensure_freshness env =
+ (* We anonymize declarations which we know will not be used *)
+ (* This assumes that the original context had no rels *)
+ process_rel_context
+ (fun d e -> EConstr.push_rel (Context.Rel.Declaration.set_name Anonymous d) e) env
+
(* Raise Not_found if not in interpretation sign *)
let try_interp_ltac_var coerce ist env {loc;v=id} =
let v = Id.Map.find id ist.lfun in
@@ -1740,15 +1746,15 @@ and interp_atomic ist tac : unit Proofview.tactic =
| AllOccurrences | NoOccurrences -> true
| _ -> false
in
- let c_interp patvars sigma =
+ let c_interp patvars env 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
if is_onhyps && is_onconcl
- then interp_type ist (pf_env gl) sigma c
- else interp_constr ist (pf_env gl) sigma c
+ then interp_type ist env sigma c
+ else interp_constr ist env sigma c
in
Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
end
@@ -1761,11 +1767,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
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 =
+ let c_interp patvars env sigma =
let lfun' = Id.Map.fold (fun id c lfun ->
Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
+ let env = ensure_freshness env in
let ist = { ist with lfun = lfun' } in
try
interp_constr ist env sigma c
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index c3d063cff8..85081b24a3 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -27,7 +27,7 @@ open Stdarg
let eval_tactic name =
let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
- let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in
+ let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in
let tac = Tacenv.interp_ltac kn in
Tacinterp.eval_tactic tac
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b05e1e85b7..0734654abf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -266,7 +266,7 @@ let my_reference c =
let znew_ring_path =
DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
let zltac s =
- lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s))
+ lazy(KerName.make (ModPath.MPfile znew_ring_path) (Label.make s))
let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);;
let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -760,7 +760,7 @@ let new_field_path =
DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
let field_ltac s =
- lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s))
+ lazy(KerName.make (ModPath.MPfile new_field_path) (Label.make s))
let _ = add_map "field"
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index f23433f2f4..2af917b939 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -337,9 +337,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
let elim, _ = destConst elim in
- let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in
+ let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
mkConst c1', gl in
let elim = EConstr.of_constr elim in
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 53153198f9..8ee6fbf036 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -24,7 +24,6 @@ open Coqlib
exception Non_closed_ascii
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
let is_gr c gr = match DAst.get c with
@@ -32,10 +31,12 @@ let is_gr c gr = match DAst.get c with
| _ -> false
let ascii_module = ["Coq";"Strings";"Ascii"]
+let ascii_modpath = MPfile (make_dir ascii_module)
let ascii_path = make_path ascii_module "ascii"
-let ascii_kn = make_kn ascii_module "ascii"
+let ascii_label = Label.make "ascii"
+let ascii_kn = MutInd.make2 ascii_modpath ascii_label
let path_of_Ascii = ((ascii_kn,0),1)
let static_glob_Ascii = ConstructRef path_of_Ascii
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 49497aef54..776d2a2229 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -33,12 +33,10 @@ let is_gr c gr = match DAst.get c with
| GRef (r, _) -> GlobRef.equal r gr
| _ -> false
+let positive_modpath = MPfile (make_dir binnums)
let positive_path = make_path binnums "positive"
-(* TODO: temporary hack *)
-let make_kn dir id = Globnames.encode_mind dir id
-
-let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
+let positive_kn = MutInd.make2 positive_modpath (Label.make "positive")
let glob_positive = IndRef (positive_kn,0)
let path_of_xI = ((positive_kn,0),1)
let path_of_xO = ((positive_kn,0),2)
@@ -74,7 +72,7 @@ let rec bignat_of_pos c = match DAst.get c with
(**********************************************************************)
let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
+let z_kn = MutInd.make2 positive_modpath (Label.make "Z")
let glob_z = IndRef (z_kn,0)
let path_of_ZERO = ((z_kn,0),1)
let path_of_POS = ((z_kn,0),2)
@@ -106,12 +104,10 @@ let bigint_of_z c = match DAst.get c with
(**********************************************************************)
let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
+let r_modpath = MPfile (make_dir rdefinitions)
let r_path = make_path rdefinitions "R"
-(* TODO: temporary hack *)
-let make_path dir id = Globnames.encode_con dir (Id.of_string id)
-
-let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
+let glob_IZR = ConstRef (Constant.make2 r_modpath @@ Label.make "IZR")
let r_of_int ?loc z =
DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 7478c1e978..703b40dd3e 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -24,9 +24,10 @@ exception Non_closed_string
let string_module = ["Coq";"Strings";"String"]
+let string_modpath = MPfile (make_dir string_module)
let string_path = make_path string_module "string"
-let string_kn = make_kn string_module "string"
+let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
let static_glob_EmptyString = ConstructRef ((string_kn,0),1)
let static_glob_String = ConstructRef ((string_kn,0),2)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 08:00:37 +0000