diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 238a1a0c5..cec0be893 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -344,9 +344,11 @@ let useInversionLemma = let gentac = hide_tactic "UseInversionLemma" (function - | [Identifier id;Command com] -> + | [Identifier id; Command com] -> fun gls -> lemInv id (pf_interp_constr gls com) gls - | l -> anomaly "useInversionLemma" l) + | [Identifier id; Constr c] -> + fun gls -> lemInv id c gls + | _ -> anomaly "useInversionLemma") in fun id com -> gentac [Identifier id;Command com] |