diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 01:38:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-15 17:45:55 +0100 |
| commit | 53f5cc210da4debd5264d6d8651a76281b0b4256 (patch) | |
| tree | 8e1edbb93c15a88480c8bc4454cc9b8fc15c88c1 /tactics/leminv.ml | |
| parent | c75619228e1c878644edbc49c5cb690777966863 (diff) | |
[econstr] Switch constrintern API to non-imperative style.
We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step
desirable to progress with EConstr there.
Diffstat (limited to 'tactics/leminv.ml')
| -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 |