coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| * \| \| \|	[sphinx] Replace remaining `@natural` by `@num`.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] More use of cmd references in Extraction chapter.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Use references for command Info.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] More reference fixes.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Fix a porting mistake.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Use references for Print.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Fix error messages and make them consistent.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	All the error messages start with a capitalized letter and end with a dot.
\| \| \| * \| \| \|	Add direct reference to congruence with.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Clean-up around options.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
\| \| \| * \| \| \|	debug trivial and debug auto were not in the tactic index.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Fix failing example in refman.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Fix some references.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Use option direct reference.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Fix a typo that appeared during the migration.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Fix a hardcoded reference.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	[sphinx] Backport reformulation.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
\| \| \| * \| \| \|	[sphinx] Backport fix of typo.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(cf. 6131f89f6b91c45e641dd877df8719fa77987453)
\| \| \| * \| \| \|	Fix typo in Coercions chapter.	Théo Zimmermann	2018-05-05
\| \|_\|/ / / / \|/\| \| \| \| \|
\| * \| \| \| \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* \| \| \| \| \|	Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.	Emilio Jesus Gallego Arias	2018-05-04
\|\ \ \ \ \ \ \| \|/ / / / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Fix #7413: coqdep warning on repeated files	Gaëtan Gilbert	2018-05-04
\| \|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The same warning exists in ocamllibdep so I copied the change there. Detecting when 2 paths are the same is approximate, eg ././a.ml and a.ml are considered different. Implementing realpath probably isn't worth doing for this warning.
* \| \| \| \| \|	Merge PR #7134: When an error comes from loading the prelude, tell it ↵	Emilio Jesus Gallego Arias	2018-05-03
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	happened at initialization time
* \ \ \ \ \ \	Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_subst	Pierre-Marie Pédrot	2018-05-03
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Fix #7415. Printing Width was not applied to error messages.	Pierre Courtieu	2018-05-03
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7304: Make `intro`/`intros` progress on existential variables.	Pierre-Marie Pédrot	2018-05-03
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Fixes issue #7083 / Windows build: Unify build logging to console (for ↵	Michael Soegtrop	2018-05-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	appveyor) and files
\| \| \| \| \| \| * \|	Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomly	Michael Soegtrop	2018-05-03
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7400: ci-vst.sh: use -o progs	Emilio Jesus Gallego Arias	2018-05-03
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7402: [ci]: add pidetop (fix #7336)	Emilio Jesus Gallego Arias	2018-05-03
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Making explicit that errors happen in one of five executation phases.	Hugo Herbelin	2018-05-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase.
\| \| \| \| \| * \| \| \|	Reporting when an error occurs at initialization time.	Hugo Herbelin	2018-05-02
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Done by simplifying the three "try" liable to be caught at initialization time into one and by ensuring that the remaining one reports about being in initialization phase.
\| \| \| * \| \| \| \|	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	[ci]: add pidetop (fix #7336)	Enrico Tassi	2018-05-02
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7339: [api] Move bullets and goals selectors to `proofs/`	Théo Zimmermann	2018-05-02
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7403: Makefile doc owners	Théo Zimmermann	2018-05-02
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Fix Makefile.ci pattern in CODEOWNERS	Maxime Dénès	2018-05-02
\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Make doc owners also own Makefile.doc	Maxime Dénès	2018-05-02
\|/ / / / / / / /
* \| \| \| \| \| \| \|	Merge PR #7394: [ci] [travis] Install num by default in all switches.	Gaëtan Gilbert	2018-05-02
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7370: Fix PHONY typo in coq_makefile	Enrico Tassi	2018-05-02
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7305: [toplevel] improve indentation	Emilio Jesus Gallego Arias	2018-05-01
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \|	ci-vst.sh: use -o progs	Gaëtan Gilbert	2018-05-01
\| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is closer to what we mean than reproducing the default target without progs.
* \| \| \| \| \| \| \| \|	Merge PR #7397: [ci] Fix #7396: VST is broken	Gaëtan Gilbert	2018-05-01
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	[ci] Fix #7396: VST is broken	Emilio Jesus Gallego Arias	2018-05-01
\|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is due to our CI script relying on their makefile internals, unfortunately we still have to do this to avoid timeouts.
\| \| \| \| * / / / /	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
\| \| \| * \| \| \| \|	[ci] [travis] Install num by default in all switches.	Emilio Jesus Gallego Arias	2018-04-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This makes sense and simplifies the script a bit. In preparation for a more uniform, Docker-based base image.
* \| \| \| \| \| \| \|	Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives.	Théo Zimmermann	2018-04-30
\|\ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #6935: Separate universe minimization and evar normalization functions	Pierre-Marie Pédrot	2018-04-30
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6944: Strict focusing using Default Goal Selector.	Pierre-Marie Pédrot	2018-04-30
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7355: [owners] Makefile.ci belongs to the CI category.	Maxime Dénès	2018-04-30
\|\ \ \ \ \ \ \ \ \ \