coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
\|
*	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\|
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\|
*	Micromega: do not use Filename.temp_dir_path, remove unused values	Gaetan Gilbert	2017-04-27
\|
*	Remove unused constructors	Gaetan Gilbert	2017-04-27
\|
*	Add [_] prefix to unused values which maybe should be kept	Gaetan Gilbert	2017-04-27
\|
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
\|
*	Rename Sos_lib.(\|\|) -> parser_or to avoid (deprecated) Pervasives.or	Gaetan Gilbert	2017-04-27
\|
*	Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum	Gaetan Gilbert	2017-04-27
\|
*	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\|
*	Remove unused [rec] keywords	Gaetan Gilbert	2017-04-27
\|
*	Merge PR#568: Remove tactic compatibility layer	Maxime Dénès	2017-04-27
\|\
* \	Merge PR#578: Fix nsatz not recognizing real literals.	Maxime Dénès	2017-04-25
\|\ \
\| \| *	Removing various tactic compatibility layers in core tactics.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Porting the firstorder plugin to the new tactic API.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Removing tactic compatibility layer in congruence.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Removing tactic compatibility layer in Micromega.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Fix the API of the new pf_constr_of_global.	Pierre-Marie Pédrot	2017-04-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead.
\| \| *	Removing trivial compatibility layer in refl_omega.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Porting omega to the new tactic API.	Pierre-Marie Pédrot	2017-04-24
\| \| \|
\| \| *	Removing trivial compatibility layer in omega.	Pierre-Marie Pédrot	2017-04-24
\| \|/ \|/\|
* \|	Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.	Maxime Dénès	2017-04-24
\|\ \
* \ \	Merge PR#565: Remove VernacError	Maxime Dénès	2017-04-24
\|\ \ \
* \ \ \	Merge branch v8.6 into trunk	Hugo Herbelin	2017-04-22
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
\| \| * \| \|	Remove VernacError	Gaetan Gilbert	2017-04-21
\| \|/ / / \|/\| \| \|
\| \| * \|	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias	2017-04-21
\| \|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
\| \| *	Fix nsatz not recognizing real literals.	Guillaume Melquiond	2017-04-20
\| \|/ \|/\|
* \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\ \
* \| \|	Silence a few OCaml warnings.	Guillaume Melquiond	2017-04-13
\| \| \|
* \| \|	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\ \ \
\| * \| \|	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove `edit_id` from the STM. In PIDE they serve a different purpose, however in Coq they were of limited utility and required many special cases all around the code. Indeed, parsing is not an asynchronous operation in Coq, thus having feedback about parsing didn't make much sense. All clients indeed ignore such feedback and handle parsing in a synchronous way. XML protocol clients are unaffected, they rely on the instead on the Fail value. This commit supersedes PR#203.
* \| \| \|	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of ↵	Maxime Dénès	2017-04-12
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	record fields.
* \ \ \ \	Merge PR#532: Clean Nsatz implementation.	Maxime Dénès	2017-04-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| * \| \| \|	Fix an algorithmic issue in Nsatz.	Pierre-Marie Pédrot	2017-04-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We use heaps instead of continuously adding elements to an ordered list, which was quadratic in the worst case. As a byproduct, this solves bug #5359, which was due to a stack overflow on big lists.
\| \| * \| \| \|	Academic prescriptivism strikes back: down with baroque programming in Nsatz.	Pierre-Marie Pédrot	2017-04-09
\| \|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Several cleanups were performed. 1. Removal of dead code lurking around. 2. Removal of global variables used to pass arguments to functions, as well as unnecessary mutable state here and there. We rely on state-passing and encapsulated mutable state. 3. Removal of crazy reference manipulation and its replacement with proper list handling, as well as cleaning up the source and taking advantage of invariants. This should solve algorithmic limitations of the previous code. 4. Opacification of some structures to have a clearer idea of the code requirements. 5. Cleaning of debug printing functions. We thunk the computation of the debugging data, whose computation can be costly for no reason, and we rely on Feedback-based interaction instead of Printf-debugging.
\| * \| \| \|	Fix an unhandled exception in Omega.	Pierre-Marie Pédrot	2017-04-07
\| \| \| \| \|
\| * \| \| \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\| \|\ \ \ \
* \| \| \| \| \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes.
* \| \| \| \|	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Fix a normalization hotspot in computation of constr keys.	Pierre-Marie Pédrot	2017-04-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Getting a key only needs to observe the root of a term. This hotspot was observed in HoTT.
\| \| \| \| \| \| *	end of correction of bug 4306	Julien Forest	2017-04-04
\| \| \| \| \| \| \|
\| \| \| \| \| \| *	Bad correction in previous commit	Julien Forest	2017-04-04
\| \| \| \| \| \| \|
\| \| \| \| \| \| *	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest	2017-04-04
\| \| \| \| \| \|/
\| \| \| * \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \| \| \|\ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
* \| \| \| \| \|	Merge PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\|\ \ \ \ \ \
\| \| \| \| * \| \|	Using delayed universe instances in EConstr.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* \| \| \| \| \| \|	Declaring ltac plugin, so that static linking works.	Hugo Herbelin	2017-04-01
\| \| \| \| \| \| \|
\| \| \| \| * \| \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For now we only normalize sorts, and we leave instances for the next commit.