diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-02-28 21:10:38 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-04 18:00:10 +0200 |
| commit | 31a35fe712a836c90562edebc01bfcf3d1c6646a (patch) | |
| tree | 754b49914270d0ea219a46dc097c260db95a7d4d /tactics/leminv.ml | |
| parent | 9a86eda0766fcc405b57183854c5095cc14cffaa (diff) | |
[econstr] Remove some Unsafe.to_constr use.
Most of it seems straightforward.
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index f47e6b2cd..10937322e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = let c = fill_holes pfterm in (* warning: side-effect on ownSign *) let invProof = it_mkNamedLambda_or_LetIn c !ownSign in - let invProof = EConstr.Unsafe.to_constr invProof in - let p = Evarutil.nf_evars_universes sigma invProof in - p, sigma + let p = EConstr.to_constr sigma invProof in + p, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in |