coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	rename test files (do not start by a digit)	Vincent Laporte

2018-01-17	Use let-in aware prod_applist_assum in dtauto and firstorder.	Jasper Hugunin
	Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).