From 27d83a1b2adf3b159a059a19ba2148118d883ac0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Apr 2024 14:16:18 +0200 Subject: [PATCH] Adapt to coq/coq#18938 (EConstr.ERelevance) --- src/ltacrecord.ml | 2 +- src/naiveknn_subst_learner.ml | 2 +- src/tactic_learner.mli | 3 ++- src/tactic_learner_internal.ml | 4 +++- 4 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ltacrecord.ml b/src/ltacrecord.ml index 314fbee2..c95cf297 100644 --- a/src/ltacrecord.ml +++ b/src/ltacrecord.ml @@ -759,7 +759,7 @@ let benchmarkSearch name time deterministic : unit Proofview.tactic = let tstring = synthesize_tactic env witness in let err = match err with | `Type_error (env, sigma, err) -> - Himsg.explain_type_error env sigma @@ Type_errors.map_ptype_error EConstr.of_constr err + Himsg.explain_type_error env sigma @@ Pretype_errors.of_type_error err | `Pretype_error (env, sigma, err) -> Himsg.explain_pretype_error env sigma err in let msg = Pp.(str "Typing failure of the following tactic:" ++ fnl () ++ tstring ++ fnl () ++ str "Typing error:" ++ fnl () ++ err) in diff --git a/src/naiveknn_subst_learner.ml b/src/naiveknn_subst_learner.ml index cb3d4dd0..6feabb9c 100644 --- a/src/naiveknn_subst_learner.ml +++ b/src/naiveknn_subst_learner.ml @@ -12,7 +12,7 @@ module NaiveKnnSubst (SF : sig type second_feat end) = functor (TS : TacticianSt type db_entry = { features : feature list; - context : (second_feat list, second_feat list) Context.Named.pt; + context : (second_feat list, second_feat list, TS.relevance) Context.Named.pt; obj : tactic; substituted_hash : int } diff --git a/src/tactic_learner.mli b/src/tactic_learner.mli index 77c65509..607ba592 100644 --- a/src/tactic_learner.mli +++ b/src/tactic_learner.mli @@ -12,7 +12,8 @@ type sexpr = Sexpr.sexpr = Node of sexpr list | Leaf of string module type TacticianStructures = sig type term - type named_context = (term, term) Context.Named.pt + type relevance + type named_context = (term, term, relevance) Context.Named.pt val term_sexpr : term -> sexpr val term_repr : term -> constr diff --git a/src/tactic_learner_internal.ml b/src/tactic_learner_internal.ml index 91f79e5a..815f7b88 100644 --- a/src/tactic_learner_internal.ml +++ b/src/tactic_learner_internal.ml @@ -19,7 +19,8 @@ let tactic_make tac = tac, Lazy.from_val (Hashtbl.hash_param 255 255 (tactic_nor module type TacticianStructures = sig type term - type named_context = (term, term) Named.pt + type relevance + type named_context = (term, term, relevance) Named.pt val term_sexpr : term -> sexpr val term_repr : term -> constr @@ -65,6 +66,7 @@ end module TS = struct type term = constr + type relevance = Sorts.relevance type named_context = Constr.named_context let term_sexpr t = constr2s t let term_repr t = t