diff options
| -rw-r--r-- | tactics/refine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index 38df13e3af..bfab02064e 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -284,7 +284,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = refine c gl (* abstraction => intro *) - | Lambda (Name id,_,m), _ + | Lambda (Name id,_,m), _ -> assert (isMeta (strip_outer_cast m)); begin match sgp with | [None] -> introduction id gl |