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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 35efb0b65..ca65f08ec 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -357,7 +357,7 @@ let refine_tac {Glob_term.closure=closure;term=term} = Pretyping.ltac_idents = closure.Glob_term.idents; } in let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in - Tactics.New.refine ~unsafe:false update + Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable end TACTIC EXTEND refine |