diff options
Diffstat (limited to 'tactics/decl_interp.ml')
| -rw-r--r-- | tactics/decl_interp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index beda246298..209d5f52f9 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -149,8 +149,8 @@ let decompose_eq env id = let get_eq_typ info env = let last_id = match info.pm_last with - Anonymous -> error "no previous equality" - | Name id -> id in + None -> error "no previous equality" + | Some (id,_) -> id in let typ = decompose_eq env last_id in typ |