diff options
| author | Emilio Jesus Gallego Arias | 2020-05-17 05:01:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-17 15:32:08 +0200 |
| commit | 3658ae24886eb42b62243ded5beca059363971f1 (patch) | |
| tree | 64ca0ca2e1b913afbc9fe5553b01cc8d178f08e0 | |
| parent | 14f0e5059e7f49cabbcd1571d7f053db7d7d3f35 (diff) | |
[leminv] Remove unused catch.
| -rw-r--r-- | plugins/ltac/leminv.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 0024d1a4ba..9841d3a14c 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -246,11 +246,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in - try - add_inversion_lemma ~poly na env sigma c sort bool tac - with - | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) - user_err ~hdr:"Inv needs Nodep Prop Set" s + add_inversion_lemma ~poly na env sigma c sort bool tac (* ================================= *) (* Applying a given inversion lemma *) |