diff options
| author | Pierre-Marie Pédrot | 2016-10-26 13:07:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-10-26 13:07:34 +0200 |
| commit | 4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (patch) | |
| tree | 15ff7464cc5a250fbb6ed2a10887d34cfb62a8a4 /tactics | |
| parent | 95429d01a8f47f5f9d1ecee3b452d920e1e1af22 (diff) | |
| parent | 2290dbb9c95b63e693ced647731623e64297f5c8 (diff) | |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 893f33f1a8..d2e5d8525d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4975,7 +4975,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=Some []; concl_occs=AllOccurrences } + {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = Refine.refine ?unsafe c <*> |