aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_check.ml2
-rw-r--r--engine/termops.ml8
-rw-r--r--engine/termops.mli3
-rw-r--r--kernel/environ.ml4
-rw-r--r--kernel/environ.mli4
-rw-r--r--kernel/type_errors.ml40
-rw-r--r--kernel/type_errors.mli3
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/pretyping.ml13
-rw-r--r--pretyping/typing.ml6
-rw-r--r--test-suite/bugs/closed/bug_9527.v1
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml41
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/vernacentries.ml2
15 files changed, 77 insertions, 56 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml
index 1f636c531a..2949adde73 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_check.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml
@@ -6,7 +6,7 @@ let simple_check1 value_with_constraints =
(* The point of renaming is to make sure the bound names printed by Check
can be re-used in `apply with` tactics that use bound names to
refer to arguments. *)
- let j = Termops.on_judgment EConstr.of_constr
+ let j = Environ.on_judgment EConstr.of_constr
(Arguments_renaming.rename_typing (Global.env())
(EConstr.to_constr evd evalue)) in
let {Environ.uj_type=x}=j in x
diff --git a/engine/termops.ml b/engine/termops.ml
index 579100ad4c..2f766afaa6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1417,11 +1417,9 @@ let prod_applist_assum sigma n c l =
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
-(* Combinators on judgments *)
-
-let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
-let on_judgment_value f j = { j with uj_val = f j.uj_val }
-let on_judgment_type f j = { j with uj_type = f j.uj_type }
+let on_judgment = Environ.on_judgment
+let on_judgment_value = Environ.on_judgment_value
+let on_judgment_type = Environ.on_judgment_type
(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in
variables skips let-in's; let-in's in the middle are put in ctx2 *)
diff --git a/engine/termops.mli b/engine/termops.mli
index 61a6ec1cd6..dea59e9efc 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -295,8 +295,11 @@ val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option
(** Combinators on judgments *)
val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment]."]
val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_value]."]
val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+[@@ocaml.deprecated "Use [Environ.on_judgment_type]."]
(** {5 Debug pretty-printers} *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 886d6b1feb..ab046f02f7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -682,6 +682,10 @@ type ('constr, 'types) punsafe_judgment = {
uj_val : 'constr;
uj_type : 'types }
+let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
+let on_judgment_value f j = { j with uj_val = f j.uj_val }
+let on_judgment_type f j = { j with uj_type = f j.uj_type }
+
type unsafe_judgment = (constr, types) punsafe_judgment
let make_judge v tj =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index a9e0717559..0df9b91c4a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -317,6 +317,10 @@ type ('constr, 'types) punsafe_judgment = {
uj_val : 'constr;
uj_type : 'types }
+val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+
type unsafe_judgment = (constr, types) punsafe_judgment
val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index fd050085d7..964d32c6b3 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -144,3 +144,43 @@ let error_unsatisfied_constraints env c =
let error_undeclared_universe env l =
raise (TypeError (env, UndeclaredUniverse l))
+
+let map_pguard_error f = function
+| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
+| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
+| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2)
+| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n
+| CodomainNotInductiveType c -> CodomainNotInductiveType (f c)
+| NestedRecursiveOccurrences -> NestedRecursiveOccurrences
+| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c)
+| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c)
+| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c)
+| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c)
+| RecCallInCaseFun c -> RecCallInCaseFun (f c)
+| RecCallInCaseArg c -> RecCallInCaseArg (f c)
+| RecCallInCasePred c -> RecCallInCasePred (f c)
+| NotGuardedForm c -> NotGuardedForm (f c)
+| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
+
+let map_ptype_error f = function
+| UnboundRel n -> UnboundRel n
+| UnboundVar id -> UnboundVar id
+| NotAType j -> NotAType (on_judgment f j)
+| BadAssumption j -> BadAssumption (on_judgment f j)
+| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
+| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar)
+| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
+| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
+| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
+| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
+| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
+| ActualType (j, t) -> ActualType (on_judgment f j, f t)
+| CantApplyBadType ((n, c1, c2), j, vj) ->
+ CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
+| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
+| IllFormedRecBody (ge, na, n, env, jv) ->
+ IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv)
+| IllTypedRecBody (n, na, jv, t) ->
+ IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
+| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+| UndeclaredUniverse l -> UndeclaredUniverse l
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3e954d6a8e..4b832930e1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -130,3 +130,6 @@ val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
val error_undeclared_universe : env -> Univ.Level.t -> 'a
+
+val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
+val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 9e93c470b1..2329b87acc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -434,7 +434,7 @@ let inh_tosort_force ?loc env evd j =
try
let t,p = lookup_path_to_sort_from env evd j.uj_type in
let evd,j1 = apply_coercion env evd p j t in
- let j2 = on_judgment_type (whd_evar evd) j1 in
+ let j2 = Environ.on_judgment_type (whd_evar evd) j1 in
(evd,type_judgment env evd j2)
with Not_found | NoCoercion ->
error_not_a_type ?loc env evd j
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46e463512d..a92b245b91 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -103,6 +103,12 @@ let search_guard ?loc env possible_indexes fixdefs =
user_err ?loc ~hdr:"search_guard" (Pp.str errmsg)
with Found indexes -> indexes)
+let esearch_guard ?loc env sigma indexes fix =
+ let fix = nf_fix sigma fix in
+ try search_guard ?loc env indexes fix
+ with TypeError (env,err) ->
+ raise (PretypeError (env,sigma,TypingError (map_ptype_error of_constr err)))
+
(* To force universe name declaration before use *)
let is_strict_universe_declarations =
@@ -597,11 +603,8 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
vn)
in
let fixdecls = (names,ftys,fdefs) in
- let indexes =
- search_guard
- ?loc !!env possible_indexes (nf_fix sigma fixdecls)
- in
- make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
+ let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in
+ make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let fixdecls = (names,ftys,fdefs) in
let cofix = (i, fixdecls) in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e8d935fcbb..2e50e1ab3f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -244,10 +244,10 @@ let judge_of_type u =
uj_type = EConstr.mkType uu }
let judge_of_relative env v =
- Termops.on_judgment EConstr.of_constr (judge_of_relative env v)
+ Environ.on_judgment EConstr.of_constr (judge_of_relative env v)
let judge_of_variable env id =
- Termops.on_judgment EConstr.of_constr (judge_of_variable env id)
+ Environ.on_judgment EConstr.of_constr (judge_of_variable env id)
let judge_of_projection env sigma p cj =
let pty = lookup_projection p env in
@@ -307,7 +307,7 @@ let type_of_constructor env sigma ((ind,_ as ctor),u) =
sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
let judge_of_int env v =
- Termops.on_judgment EConstr.of_constr (judge_of_int env v)
+ Environ.on_judgment EConstr.of_constr (judge_of_int env v)
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
where both the term and type are in n.f. *)
diff --git a/test-suite/bugs/closed/bug_9527.v b/test-suite/bugs/closed/bug_9527.v
new file mode 100644
index 0000000000..e08d194c6c
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9527.v
@@ -0,0 +1 @@
+Fail Check fix f (x : nat) := (let x := (f x) in f 0).
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 42b313f200..06428b53f2 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -58,7 +58,7 @@ let process_vernac_interp_error exn = match fst exn with
mt() in
wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- let te = Himsg.map_ptype_error EConstr.of_constr te in
+ let te = map_ptype_error EConstr.of_constr te in
wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index f78b43e2fa..367fa4ce98 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1297,45 +1297,8 @@ let explain_pattern_matching_error env sigma = function
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env sigma typs
-let map_pguard_error f = function
-| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody
-| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c)
-| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2)
-| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n
-| CodomainNotInductiveType c -> CodomainNotInductiveType (f c)
-| NestedRecursiveOccurrences -> NestedRecursiveOccurrences
-| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c)
-| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c)
-| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c)
-| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c)
-| RecCallInCaseFun c -> RecCallInCaseFun (f c)
-| RecCallInCaseArg c -> RecCallInCaseArg (f c)
-| RecCallInCasePred c -> RecCallInCasePred (f c)
-| NotGuardedForm c -> NotGuardedForm (f c)
-| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c)
-
-let map_ptype_error f = function
-| UnboundRel n -> UnboundRel n
-| UnboundVar id -> UnboundVar id
-| NotAType j -> NotAType (on_judgment f j)
-| BadAssumption j -> BadAssumption (on_judgment f j)
-| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
-| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar)
-| CaseNotInductive j -> CaseNotInductive (on_judgment f j)
-| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
-| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n)
-| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2)
-| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j)
-| ActualType (j, t) -> ActualType (on_judgment f j, f t)
-| CantApplyBadType ((n, c1, c2), j, vj) ->
- CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj)
-| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv)
-| IllFormedRecBody (ge, na, n, env, jv) ->
- IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv)
-| IllTypedRecBody (n, na, jv, t) ->
- IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
-| UnsatisfiedConstraints g -> UnsatisfiedConstraints g
-| UndeclaredUniverse l -> UndeclaredUniverse l
+let map_pguard_error = map_pguard_error
+let map_ptype_error = map_ptype_error
let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 986906d303..f22354cdbf 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -44,6 +44,8 @@ val explain_module_internalization_error :
Modintern.module_internalization_error -> Pp.t
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
+[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fcb96401ee..6c4b0acd52 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1785,7 +1785,7 @@ let vernac_check_may_eval ~atts redexp glopt rc =
else
let c = EConstr.to_constr sigma c in
(* OK to call kernel which does not support evars *)
- Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
+ Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c)
in
let pp = match redexp with
| None ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:00:43 +0000