coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \|	Renaming binders into binderlists in egramcoq.ml.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Introducing an intermediary type "constr_prod_entry_key" for grammar ↵	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
\| \| \| \| * \| \| \| \| \| \|	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Minor clarifying of name variables in constrintern.ml.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- renaming lvar into ntnvars when relevant, for consistency - renaming sometimes genv into env (intern_env) so as to remain consistent with other parts of the code
\| \| \| \| * \| \| \| \| \| \|	Using name given by user to name a 'pat, if any.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This works for contexts in Definition and co, but not yet for "fun" and co.
\| \| \| \| * \| \| \| \| \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
\| \| \| \| * \| \| \| \| \| \|	Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Notations: Do not consider a non-occurring variable as a binder-only variable.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \|	Adding support for re-folding notation referring to isolated "forall '(x,y), t".	Hugo Herbelin	2018-02-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was apparently forgotten in a67bd7f9.
\| \| \| \| * \| \| \| \| \| \|	Again one more step in fixing #5762 ("where" clause).	Hugo Herbelin	2018-02-20
\| \|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We enforce that variables of the notation hide the variables in the implicit-arguments map. Will be useful when there will be a special map of single binders when interpreting notations.
\| \| \| \| * \| \| \| \| \|	ci: add elpi	Enrico Tassi	2018-02-19
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	record: restore API declare_projections (removed in e414c07e1)	Enrico Tassi	2018-02-19
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	constraints.
* \ \ \ \ \ \ \ \ \	Merge PR #6761: Remove unused argument in Record.declare_structure	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6753: [toplevel] Make toplevel state into a record.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \|	Fix #6529: nf_evar_info and check the env evars' not just the concl	Matthieu Sozeau	2018-02-19
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6230: Better Cemitcodes API + compact relocation representation	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6772: Cleanup inferCumulativity	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6648: [tactics] make apply_type safe	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	camlp4
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6571: Fix ci-all target	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	longer use camlp4.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	No using a mutable counter to skip them, instead we keep them in the environment.
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \|_\|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Adding a test for the construction that was broken in Coccinelle.	Pierre-Marie Pédrot	2018-02-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There was no test in the test-suite checking for double with-def constraints in module typing.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We defer the computation of the universe quantification to the upper layer, outside of the kernel.
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Adding a test for variance subtyping in the module system.	Pierre-Marie Pédrot	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Adding a sanity check on inductive variance subtyping.	Pierre-Marie Pédrot	2018-02-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[toplevel] Make toplevel state into a record.	Emilio Jesus Gallego Arias	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \|	[ide] Localize a IDE-specific flag.	Emilio Jesus Gallego Arias	2018-02-15
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #1073: new quick2vo target: like vio2vo, but smarter	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	disable tests: vio2vo is broken in Windows	Ralf Jung	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	also test vio2vo	Ralf Jung	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	test "make quick2vo"	Ralf Jung	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	new quick2vo target: like vio2vo, but smarter	Ralf Jung	2018-02-15
\| \| \|_\|_\|/ / / / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coq_makefile: Support "" as the prefix in _CoqProject	Joachim Breitner	2018-02-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #6760: CHANGES for 8.7.2.	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Extend `zify_N` with knowledge about `N.pred`	Joachim Breitner	2018-02-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	CHANGES for 8.7.2.	Théo Zimmermann	2018-02-14
\|/ / / / / / / / / / / / / / / /
\| \| \| \| \| \| \| \| \| * / / / / / /	Remove unused argument in Record.declare_structure	Gaëtan Gilbert	2018-02-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was for autoinstance.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Factorize the relocations in the on-disk VM representation.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of using a linear representation, we simply use a table that maps every kind of relocation to the list of positions it needs to be applied to.
\| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Use a more compact representation for bytecode relocations stored on disk.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The previous implementation used a list of pairs, which has size 9n where n is the number of relocations. We instead use two arrays for a total memory cost of 2n + 5 words. The use of arrays may turn out to be problematic on 32-bit machines, I am unsure if we will hit this limitation in practice.