coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-11-02	Remove is_universe_polymorphism from printing	Gaëtan Gilbert

2018-02-20	Using name given by user to name a 'pat, if any.	Hugo Herbelin
	This works for contexts in Definition and co, but not yet for "fun" and co.
2018-02-20	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin
	The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
2017-03-23	A test checking for non-collision of name in irrefutable patterns.	Hugo Herbelin

2016-07-19	Some extra fixes in printing patterns in binders.	Hugo Herbelin
	- typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
2016-07-19	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin
	Supporting accordingly printing of sequences of binders including binding patterns.
2016-07-19	Fixing missing parentheses in printing of patterns in binders.	Hugo Herbelin
	(In agreement with Daniel.)
2016-06-27	Patterns in binders: printing tests	Arnaud Spiwack