aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evarutil.ml17
-rw-r--r--engine/logic_monad.ml8
-rw-r--r--engine/namegen.ml11
-rw-r--r--engine/proofview.ml4
-rw-r--r--engine/termops.ml6
-rw-r--r--engine/univGen.ml14
6 files changed, 32 insertions, 28 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 911b189deb..ea71be8e43 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -331,11 +331,16 @@ let push_rel_decl_to_named_context
let map_decl f d =
NamedDecl.map_constr f d
in
- let replace_var_named_declaration id0 id decl =
- let id' = NamedDecl.get_id decl in
- let id' = if Id.equal id0 id' then id else id' in
- let vsubst = [id0 , mkVar id] in
- decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst)
+ let rec replace_var_named_declaration id0 id = function
+ | [] -> []
+ | decl :: nc ->
+ if Id.equal id0 (NamedDecl.get_id decl) then
+ (* Stop here, the variable cannot occur before its definition *)
+ (NamedDecl.set_id id decl) :: nc
+ else
+ let nc = replace_var_named_declaration id0 id nc in
+ let vsubst = [id0 , mkVar id] in
+ map_decl (fun c -> replace_vars vsubst c) decl :: nc
in
let extract_if_neq id = function
| Anonymous -> None
@@ -366,7 +371,7 @@ let push_rel_decl_to_named_context
context. Unless [id] is a section variable. *)
let subst = update_var id0 id subst in
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
- let nc = List.map (replace_var_named_declaration id0 id) nc in
+ let nc = replace_var_named_declaration id0 id nc in
(push_var id0 subst, Id.Set.add id avoid, d :: nc)
| Some id0 when hypnaming = FailIfConflict ->
user_err Pp.(Id.print id0 ++ str " is already used.")
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 2354d2c5e8..7c06bb59f1 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -41,7 +41,7 @@ let _ = CErrors.register_handler begin function
| Timeout -> CErrors.user_err ~hdr:"Some timeout function" (Pp.str"Timeout!")
| Exception e -> CErrors.print e
| TacticFailure e -> CErrors.print e
- | _ -> Pervasives.raise CErrors.Unhandled
+ | _ -> raise CErrors.Unhandled
end
(** {6 Non-logical layer} *)
@@ -70,11 +70,11 @@ struct
let map f a = (); fun () -> f (a ())
end)
- type 'a ref = 'a Pervasives.ref
+ type 'a ref = 'a Util.pervasives_ref
let ignore a = (); fun () -> ignore (a ())
- let ref a = (); fun () -> Pervasives.ref a
+ let ref a = (); fun () -> ref a
(** [Pervasives.(:=)] *)
let (:=) r a = (); fun () -> r := a
@@ -93,7 +93,7 @@ struct
let (src, info) = CErrors.push src in
h (e, info) ()
- let read_line = fun () -> try Pervasives.read_line () with e ->
+ let read_line = fun () -> try read_line () with e ->
let (e, info) = CErrors.push e in raise ~info e ()
let print_char = fun c -> (); fun () -> print_char c
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 77d45ce1e4..89c2fade62 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -24,7 +24,6 @@ open EConstr
open Vars
open Nameops
open Libnames
-open Globnames
open Context.Rel.Declaration
module RelDecl = Context.Rel.Declaration
@@ -72,7 +71,7 @@ let is_imported_modpath = function
in find_prefix (Lib.current_mp ())
| _ -> false
-let is_imported_ref = function
+let is_imported_ref = let open GlobRef in function
| VarRef _ -> false
| IndRef (kn,_)
| ConstructRef ((kn,_),_) ->
@@ -90,7 +89,7 @@ let is_global id =
let is_constructor id =
try
match Nametab.locate (qualid_of_ident id) with
- | ConstructRef _ -> true
+ | GlobRef.ConstructRef _ -> true
| _ -> false
with Not_found ->
false
@@ -102,7 +101,7 @@ let is_section_variable id =
(**********************************************************************)
(* Generating "intuitive" names from its type *)
-let global_of_constr = function
+let global_of_constr = let open GlobRef in function
| Const (c, _) -> ConstRef c
| Ind (i, _) -> IndRef i
| Construct (c, _) -> ConstructRef c
@@ -149,8 +148,8 @@ let hdchar env sigma c =
| Cast (c,_,_) | App (c,_) -> hdrec k c
| Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn)))
| Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn))
- | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
- | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.IndRef x)) with Not_found when !Flags.in_debugger -> "zz")
+ | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (GlobRef.ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz")
| Var id -> lowercase_first_char id
| Sort s -> sort_hdchar (ESorts.kind sigma s)
| Rel n ->
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c4a624e462..8b5bd4cd80 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -542,7 +542,7 @@ let tclDISPATCHGEN join tacs =
let tacs = CList.map branch tacs in
InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs)
-let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs
+let tclDISPATCH tacs = tclDISPATCHGEN ignore tacs
let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs
@@ -910,7 +910,7 @@ let tclPROGRESS t =
exception Timeout
let _ = CErrors.register_handler begin function
| Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
- | _ -> Pervasives.raise CErrors.Unhandled
+ | _ -> raise CErrors.Unhandled
end
let tclTIMEOUT n t =
diff --git a/engine/termops.ml b/engine/termops.ml
index 1ed2d93b3c..2ab2f60421 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1058,7 +1058,7 @@ let is_section_variable id =
with Not_found -> false
let global_of_constr sigma c =
- let open Globnames in
+ let open GlobRef in
match EConstr.kind sigma c with
| Const (c, u) -> ConstRef c, u
| Ind (i, u) -> IndRef i, u
@@ -1067,7 +1067,7 @@ let global_of_constr sigma c =
| _ -> raise Not_found
let is_global sigma c t =
- let open Globnames in
+ let open GlobRef in
match c, EConstr.kind sigma t with
| ConstRef c, Const (c', _) -> Constant.equal c c'
| IndRef i, Ind (i', _) -> eq_ind i i'
@@ -1379,7 +1379,7 @@ let dependency_closure env sigma sign hyps =
List.rev lh
let global_app_of_constr sigma c =
- let open Globnames in
+ let open GlobRef in
match EConstr.kind sigma c with
| Const (c, u) -> (ConstRef c, u), None
| Ind (i, u) -> (IndRef i, u), None
diff --git a/engine/univGen.ml b/engine/univGen.ml
index a347bba188..b1ed3b2694 100644
--- a/engine/univGen.ml
+++ b/engine/univGen.ml
@@ -56,15 +56,15 @@ let fresh_global_instance ?loc ?names env gr =
u, ctx
let fresh_constant_instance env c =
- let u, ctx = fresh_global_instance env (ConstRef c) in
+ let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
(c, u), ctx
let fresh_inductive_instance env ind =
- let u, ctx = fresh_global_instance env (IndRef ind) in
+ let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
(ind, u), ctx
let fresh_constructor_instance env c =
- let u, ctx = fresh_global_instance env (ConstructRef c) in
+ let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
(c, u), ctx
let fresh_global_instance ?loc ?names env gr =
@@ -84,10 +84,10 @@ let fresh_global_or_constr_instance env = function
let global_of_constr c =
match kind c with
- | Const (c, u) -> ConstRef c, u
- | Ind (i, u) -> IndRef i, u
- | Construct (c, u) -> ConstructRef c, u
- | Var id -> VarRef id, Instance.empty
+ | Const (c, u) -> GlobRef.ConstRef c, u
+ | Ind (i, u) -> GlobRef.IndRef i, u
+ | Construct (c, u) -> GlobRef.ConstructRef c, u
+ | Var id -> GlobRef.VarRef id, Instance.empty
| _ -> raise Not_found
let fresh_sort_in_family = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 22:37:26 +0000