[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v (#275)

* [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v

It's rather verbose, unfortunately.  The reification also doesn't have
any of the nice debugging features of the version of reification in
Compilers, because that's even more boilerplate.  Not sure if I should
add that back in, at the moment.

Also, for some strange reason, places where `constr`s fail to typecheck
seem to induce backtracking where I don't think they should, and I'm not
sure what's going on...

* [demo] Add more namespacing

* Update llet notation, update is_known_const name

As per code review suggestions

* Namespace var_context, add some coqbug references

* Rename is_type_arg to is_template_parameter

As per https://github.com/mit-plv/fiat-crypto/pull/275#discussion_r153036059

* Simplify the logic around delayed arguments a bit

We no longer pass around dummy markers in the tuple of arguments.

* [demo] More informative reification error messages

This time without exponential slowdown in failure cases and without
needing to manually think up all of the possible errors and write them
out.

Possible thanks to Hugo's comment at
https://github.com/coq/coq/issues/6252#issuecomment-347041995

* [demo] respond to code review, add comments

* Update documentation with suggestions from Andres

0 files changed, 0 insertions, 0 deletions