diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index bbc1285e2..ad2fd9009 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -277,7 +277,7 @@ let tauto_classical nnpp g = let tauto g = try - let nnpp = constr_of_global (Nametab.absolute_reference coq_nnpp_path) in + let nnpp = constr_of_global (Nametab.global_of_path coq_nnpp_path) in (* try intuitionistic version first to avoid an axiom if possible *) tclORELSE tauto_intuitionistic (tauto_classical nnpp) g with Not_found -> |