3 files changed, 8 insertions, 3 deletions
diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index f1bdd64092..bfa2d47413 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -33,6 +33,10 @@ type oblinfo =
     ev_tac: tactic option;
     ev_deps: Intset.t }
 
+(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
+open Store.Field
+let evar_tactic = Store.field ()
+
 (** Substitute evar references in t using De Bruijn indices,
   where n binders were passed through. *)
 
@@ -210,7 +214,7 @@ let eterm_obligations env name isevars evm fs ?status t ty =
 	   | Some s -> s, None
 	   | None -> Define true, None
 	 in
-	 let tac = match ev.evar_extra with
+	 let tac = match evar_tactic.get ev.evar_extra with
 	   | Some t ->
 	       if Dyn.tag t = "tactic" then
 		 Some (Tacinterp.interp 
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 0eba0f6336..e649ad97be 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -50,7 +50,7 @@ open Tacinterp
 open Tacexpr
 
 let solve_tccs_in_type env id isevars evm c typ =
-  if not (evm = Evd.empty) then
+  if not (Evd.is_empty evm) then
     let stmt_id = Nameops.add_suffix id "_stmt" in
     let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
       match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with
@@ -246,5 +246,5 @@ let subtac (loc, command) =
 	  raise e)
 
   | e ->
-      msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e);
+      msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e);
       raise e
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 1424618f00..181d0fa72d 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -489,6 +489,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
+	| Util.Anomaly _ as e -> raise e
 	| e -> false
 
 and solve_prg_obligations prg tac =