Samuel Gruetter
Samuel Gruetter
Just updated the issue title to say what I mean :wink: But I guess it's hard to detect what's text and what's Gallina if coqtop doesn't give you back something...
I see, so I guess I'll have to wait for https://github.com/QuickChick/QuickChick/issues/81 :wink:
Ah I see, and I agree that preferring simple regexes for performance reasons makes sense, because when I work on interactive proofs with large goals, it often happens that a...
When my proof scripts contain no bugs, the goals are usually quite small and printed instantly. Printing slowness occurs when I have a bug in a proof script and some...
Thanks for the quick reply! I played a bit more with `l:`, `q:`, `limit:`, and `exh:`, none of which made it work with what I tried. But `sauto depth: 3.`...
Ok, so if I do `Set Hammer ReconstrLimit 20.`, `hammer` takes about 1 minute, and succeeds by telling me to use `hecrush use: putmany_spec.`, which takes 6s.
I see, thanks :+1: I also tried to use the `hecrush` that worked on the isolated standalone example in the actual context, and there it didn't finish for several minutes....
Most of my `Prop`s are decidable, so (2) shouldn't be a problem.
> There used to be such a [tactic](https://github.com/QuickChick/QuickChick/blob/master/src/tactic_quickchick.ml4), This looks like exactly what I'd want! (except that, as you said, it doesn't currently work in 8.8, if I type `quickchick.`,...
Just ran into this as well, it's quite confusing when a file behaves differently in PG than when compiled with `coqc`...