Fix of silly bug

coq-tactician · Oct 1, 2024 · b057ec2 · b057ec2
1 parent b883ae5
commit b057ec2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/graph_extractor.ml b/src/graph_extractor.ml
@@ -340,7 +340,7 @@ module CICGraphMonad (G : GraphMonadType) : CICGraphMonadType
     let+ named = lookup_named_map in
     try
       Id.Map.find id named
-    with Not_found -> CErrors.anomaly Pp.(str "Variable name could not be resolved")
+    with Not_found -> CErrors.anomaly Pp.(str "Variable name " ++ Id.print id ++ str " could not be resolved")
   let lookup_def_depth =
     let+ { def_depth; _ } = ask in
     def_depth

diff --git a/src/neural_learner.ml b/src/neural_learner.ml
@@ -723,7 +723,7 @@ module NeuralLearner : TacticianOnlineLearnerType = functor (TS : TacticianStruc
             ((match cache_type path with
              | `File -> Feedback.msg_warning (Pp.str "Malformed proof state detected")
              | _ -> ()); true)
-          else false
+          else status
         | _ -> Constr.fold aux status c in
       let status = aux false (TS.term_repr @@ TS.proof_state_goal ps) in
       let status = Context.Named.fold_outside