diff options
| author | Hugo Herbelin | 2014-08-20 22:30:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:33 +0200 |
| commit | b006f10e7d591417844ffa1f04eeb926d6092d7b (patch) | |
| tree | 9253b32cb1adabafce28f123ef9eb11d4fa122f4 /tactics/auto.ml | |
| parent | ca300977724a6b065a98c025d400c71f41b9df4b (diff) | |
Uniformisation of the order of arguments env and sigma.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 67484429f2..e386728fe7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -912,7 +912,7 @@ let prepare_hint check env init (sigma,c) = let interp_hints poly = fun h -> let f c = - let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in + let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in prepare_hint true (Global.env()) Evd.empty (evd,c) in let fr r = let gr = global_with_alias r in |