diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /tactics/leminv.ml | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e9dace858..7eb81c3f4 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -237,7 +237,7 @@ 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 () and evd = ref Evd.empty in - let c = Constrintern.interp_type_evars evd env com in + let c = Constrintern.interp_type_evars env evd com in let sigma, sort = Pretyping.interp_sort !evd comsort in try add_inversion_lemma na env sigma c sort bool tac |