Trunk+abstracting injection flags#677

Merged

coqbot merged 2 commits into

rocq-prover:masterfrom

herbelin:trunk+abstracting-injection-flags

Oct 27, 2017

Commits on Oct 26, 2017

Delay use of flag "Discriminate Introduction" from interp to execution time.
herbelin
committed
Passing around the flag for injection so that tactics calling inj at
herbelin
committed