diff options
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 6caebf6c4f..1d6cd8e99b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -390,7 +390,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) | Unfold_nth c -> Proofview.V82.tactic (fun gl -> if exists_evaluable_reference (pf_env gl) c then - tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl + tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl else tclFAIL 0 (str"Unbound reference") gl) | Extern tacast -> conclPattern concl p tacast |