diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 10:51:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 14:42:29 +0100 |
| commit | cedcfc9bc386456f3fdd225f739706e4f7a2902c (patch) | |
| tree | c8161338a95bebdab6501606edda5a0a939da4a0 /plugins/extraction/ocaml.ml | |
| parent | 8b15e47a6b3ccae696da8e12dbad81ae0a740782 (diff) | |
Refine tactic now shelves unifiable holes.
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
Diffstat (limited to 'plugins/extraction/ocaml.ml')
0 files changed, 0 insertions, 0 deletions