diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:36:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:36:50 +0100 |
| commit | 0168ee0b6463a9ef44d768b0020b34785986c1cb (patch) | |
| tree | c3bb1d2eef4fa5edfd2d431669015db896e08633 /tactics | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
| parent | 53f5cc210da4debd5264d6d8651a76281b0b4256 (diff) | |
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 1ae3577ed..01065868d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -249,11 +249,11 @@ let add_inversion_lemma name env sigma t sort dep inv_op = let add_inversion_lemma_exn na com comsort bool tac = let env = Global.env () in - let evd = ref (Evd.from_env env) in - let c = Constrintern.interp_type_evars env evd com in - let evd, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env !evd comsort in + let sigma = Evd.from_env env in + let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in try - add_inversion_lemma na env evd c sort bool tac + add_inversion_lemma 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 |