coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[engine] Remove ghost parameter from `Proofview.Goal.t`	Emilio Jesus Gallego Arias	2018-02-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
*	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\|
*	Removing default evar-normalization for ARGUMENT EXTEND.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \|	This fixes bug 5650: evar (x : Prop) should not be slow.
*	[api] Remove type equalities from API.	Emilio Jesus Gallego Arias	2017-07-25
\| \| \| \| \| \| \| \| \| \| \| \|	This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	don't leak unqualified identifiers from the macro	Matej Košík	2017-06-10
\|
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
\|
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does not prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s$~label:"[^"]"\s$\?$Pp.$\?($\(Pp.$\?str\)\?\s".[^\.!]")' \| xargs sed s'/$anomaly\s\(~label:"[^"]"\s$\?$Pp.$\?($\(Pp.$\?str\)\?\s".\s[^\.! ]\)\s")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' \| xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly \| grep '\.ml' \| grep -v 'anomaly\s$~label:"[^"]"\s$\?$Pp\.$\?($\(Pp.$\?str\)\?\s".*$\.\\|!$")' \| grep 'anomaly$$\\|[^_]$' \| less ```
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Adding support for using grammar entries returning no value in EXTEND.	Hugo Herbelin	2017-05-16
\| \|
* \|	[location] Remove `Loc.internal_ghost`	Emilio Jesus Gallego Arias	2017-04-25
\| \| \| \| \| \| \| \| \| \|	`internal_ghost` was an artifact to ease porting of the ml4 rules. Now that the location is optional we can finally get rid of it.
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\|/ \| \| \|	Now it is a private field, locations are optional.
*	Fix compilation with camlp5 transitional mode.	Maxime Dénès	2017-04-14
\| \| \| \|	It was failing after 1d0eb5d4d6fea.
*	[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.
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Yet another Makefile reform : a unique phase without nasty make tricks	Pierre Letouzey	2016-06-01
	We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)