Adapt to coq/coq#18938 (EConstr.ERelevance)

SkySkimmer · Apr 17, 2024 · 27d83a1 · 27d83a1
1 parent 879bd87
commit 27d83a1
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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