Fix #9527: unknown evar in nonterminating [fix] error.

4 files changed, 6 insertions, 41 deletions

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 ->