aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 15:17:05 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-15 15:31:14 +0100
commit4ea9b3193eaced958bb277c0723fb54d661ff520 (patch)
tree674fe651612dc17f3bf99404fae02d58437ef5a1 /tactics/auto.ml
parent15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (diff)
More conversion functions in the new tactic API.
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6caebf6c4..1d6cd8e99 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