diff options
Diffstat (limited to 'contrib/linear/dpc.ml4')
| -rwxr-xr-x | contrib/linear/dpc.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/linear/dpc.ml4 b/contrib/linear/dpc.ml4 index ba7bc884d4..d30cf9ae1c 100755 --- a/contrib/linear/dpc.ml4 +++ b/contrib/linear/dpc.ml4 @@ -24,7 +24,7 @@ open Ccidpc let rec intros_forall gls = let t = pf_concl gls in if is_forall_term t - then ((tclTHEN forAllI (intros_forall))) gls + then ((tclTHEN intro (intros_forall))) gls else tclIDTAC gls let dPC_nq gls = |