coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-09-23	Fixes #10778 (fresh was not updated after renaming of intropattern entry in ↵	Hugo Herbelin
	#10239). The bug was introduced in #10239 which seems to have actually remained half-done: "wit_intropattern" and "wit_simple_intropattern" did not share the same representation of values (val_tag) but the code was assuming (especially the code for "fresh") that this was shared. We fix it by sharing the internal representation (`dyn` field in Tacarg.make0) as suggested by @ppedrot in the discussion of #10239 (this allows also to simplify Taccoerce.is_intro_pattern).