Port reification to Ltac2

[JasonGross]

Closes #1350

To be reviewed and merged in tandem with mit-plv/rewriter#57

Note for future reference: timing done with

export branch=ltac2-reify; export n="$(git log 9af638cfe53c76f7bf8e38b8c22464af2e587cb6..origin/ltac2-reify --oneline  | wc -l)"; for i in $(seq $((n-1)) -1 0); do spec="$branch$(for j in $(seq 1 $i); do echo -n ^; done)"; git checkout "$spec" && if ! git log -1 | grep -q 'Timing Diff'; then ./etc/coq-scripts/timing/make-pretty-timed-diff-tip.sh -j5 pre-standalone SKIP_BEDROCK2=1 && ((git log -1 --pretty=%B; echo; echo '<details><summary>Timing Diff</summary>'; echo '<p>'; echo; echo '```'; cat ./time-of-build-both.log; echo; echo '```'; echo '</p>'; echo '</details>') | git commit --amend -F - ) && export sha="$(git log -1 --pretty=%H)"; git checkout $branch && git rebase $sha; git push origin $branch:$branch -f; fi; done; git checkout $branch; git push origin $branch:$branch -f

Bumps done with

export shas="$(cd rewriter; git log jgross/ltac2-reify-incremental-001..jgross/ltac2-reify-incremental-010 --format=%H | tac)"; for sha in $shas; do (cd rewriter/; descr="Bump rewriter to$(git log $sha -1 --format="%C(auto) %h %s")"; git checkout $sha; cd ..; git commit -am "$descr"); done