coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-15	Propagating scope information in indirect application to a reference.	Hugo Herbelin
	This allows the following to interpret "0" in the expected scope: Notation "0" := true : bool_scope. Axiom f : bool -> bool -> nat. Record R := { p : bool -> nat }. Check (@f 0) 0. Check fun r => r.(@p) 0.
2020-02-25	Fixing residual bug of #11120.	Hugo Herbelin
	On the principle that a notation to a constant inherits the implicit arguments of the constant, a non-applied notation should inherit its next maximal implicit arguments.
2020-02-22	Inherit scopes and implicit sign. in notations for partially applied pattern.	Hugo Herbelin
	Exception: when the notation is to some @id. Formerly, this was ignored for all kinds of string notations.
2020-02-22	Inherit argument scopes in notations to expressions of the form @f.	Hugo Herbelin
	This is a change of semantics.
2020-02-22	Propagate implicit arguments in all notations for partial applications.	Hugo Herbelin
	This was done for abbreviations but not string notations. This adopts the policy proposed in #11091 to make parsing and printing consistent.
2020-02-22	Fixing a bug introduced in PR #10832 (new format specific to a given notation).	Hugo Herbelin
	The import of the format should not be done if i<>1 in open_notation.
2019-12-10	Fixing #10750 (anomaly of "Print Visibility" on only-printing notations).	Hugo Herbelin

2019-05-10	Use Print Custom Grammar to inspect custom entries	Jasper Hugunin

2019-02-19	Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.	Hugo Herbelin
	This is because it can raise Not_found in depth and we need to catch it at the right time.
2018-07-29	Supporting locality flag for custom entries + compatibility with modules.	Hugo Herbelin
	Also prevents to use an entry name already defined.
2018-07-29	A test on the different ways to indicate the levels of a rule.	Hugo Herbelin
	This is in preparation of changes in level_eq, to check that the semantics is preserved.
2018-02-20	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin
	Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x\|P} and {'pat\|P}.
2018-02-20	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin

2017-11-20	Fixing factorization of recursive notations in the case of an atomic separator.	Hugo Herbelin
	This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
2017-11-14	One more step in fixing #5762 ("where" clause).	Hugo Herbelin
	We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
2016-03-13	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin
	notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable).
2016-03-13	Adding a file summarizing the inconsistencies in interpreting implicit	Hugo Herbelin
	arguments and scopes with abbreviations and notations. Comments are welcome on the proposed solutions for uniformization.