coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	inductive.ml : get rid of some obvious (Lazy.force (lazy t))	letouzey	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16935 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
\| \| \| \| \| \| \| \| \|	* Using generic fold functions was unecessarily obscure * No more List.mem and hence indirect use of ocaml generic comparison * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic semantic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Specializing hash functions for widely used types.	ppedrot	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restore my version of notation_ops.ml now that List.remove_assoc_f is fixed	letouzey	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16932 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix the semantic of the new List.remove_assoc_f	letouzey	2013-10-24
\| \| \| \| \| \| \|	Unlike Ocaml's stdlib List.remove_assoc, I was raising Not_found when the key to remove wasn't there... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16931 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oups, repair the compilation (micromega + Morphism_prop)	letouzey	2013-10-24
\| \| \| \| \| \| \| \| \| \| \| \| \|	It seems I forgot to fully recompile after my last bunch of syntactic changes about List.assoc_f, that weren't so syntactic after all, sorry : - Util isn't used in micromega, hence no List.assoc_f there - There is something wrong in my modifications of Notation_ops that breaks the compilation of Morphism_prop. For the moment I don't see what, so I revert all the modifications of this file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16930 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ephemeron: add a function to run a collection cycle	gareuselesinge	2013-10-24
\| \| \| \| \| \| \| \| \| \| \| \|	This is necessary if one wants to check how much memory Coq uses after a collection. The idiom is: Gc.full_major (); Ephemeron.clear (); Gc.full_major (); since the first collection may just put collected ephemerons in a to_be_cleared list that is processed by Ephemeron.get/create/clear. Processing the list may create new garbage (the content of the ephemeron), Hence a new Gc cycle has to be run afterwards. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16929 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: fix coloring bug when jumping back to the first phrase	gareuselesinge	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Get rid of polymorphic comparison in "plugins/btauto/refl_btauto.ml".	xclerc	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16927 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Get rid of polymorphic equality in "checker/subtyping.ml".	xclerc	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16926 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList: a few alternative to hashtbl-based uniquize, distinct, subset	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CList.factorize_left with a parametric equality	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CList.prefix_of and CList.drop_prefix with a parametric equality	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16922 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tacintern: avoid a match (fst (List.hd ...))	letouzey	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16919 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small optimizations in unification.	ppedrot	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing List.mem in Namegen. We may choose a better fitted datastructure ↵	ppedrot	2013-10-23
\| \| \| \| \| \|	than lists on day... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16917 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimizing Vars.replace_vars	ppedrot	2013-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16916 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing some generic equalities.	ppedrot	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving potentially costly computation from exception raising to message	ppedrot	2013-10-22
\| \| \| \| \| \|	printing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16914 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing useless array-to-list and converse casts used in	ppedrot	2013-10-22
\| \| \| \| \| \|	Evar{conv,solve} files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16913 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimizing evar filters. It seems to cost quite a lot in unification,	ppedrot	2013-10-22
\| \| \| \| \| \| \|	as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various optimizations in Constr, such as term sharing and allocation	ppedrot	2013-10-22
\| \| \| \| \| \|	avoiding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More efficient operations in CArray.	ppedrot	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16910 85f007b7-540e-0410-9357-904b9bb8a0f7
*	STM: proper error message if the GUI edits_at a dummy state	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16909 85f007b7-540e-0410-9357-904b9bb8a0f7
*	STM: do not enrich exceptions more than once	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: always retag on insert	gareuselesinge	2013-10-22
\| \| \| \| \| \| \|	This should fix Arnaud's bug (reported by private email) that makes coq eat two sentences at once (and process only the first one). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16907 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: do not try to backtrack to a dummy id	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 85f007b7-540e-0410-9357-904b9bb8a0f7
*	emacs config: next-error search path ok even if default-directory unset.	courtieu	2013-10-22
\| \| \| \| \| \| \| \|	This way next-error behaves accordingly with make -C. Making the setting of default-directory independent of the compile/next-error setting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16905 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Wg_Find: regex + case insensitive find/replace support	gareuselesinge	2013-10-22
\| \| \| \| \| \|	It uses Str, hence it also supports captures \(..\) and \1 .. \n git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
*	wg_Detachable: move out of wg_Command	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Wg_Commands: fix warning "widget not within a GtkWindow"	gareuselesinge	2013-10-22
\| \| \| \| \| \| \|	The constructor was calling indirectly grab_default that requires the widget to be anchored. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Wg_Commands: when detached display the buffer name	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: display in the errors window also the slaves status	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
*	STM: send the gui the status of the slaves	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New feedback message: SlaveStatus	gareuselesinge	2013-10-22
\| \| \| \| \| \|	To tell the gui what a slave is doing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
*	wg_Commands: smaller icons in tabs	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ideutils: support custom size for stock icons	gareuselesinge	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
*	proof modes: use ephemerons to represent them in proof state	gareuselesinge	2013-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16895 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqtop: fix looping over a broken state.	gareuselesinge	2013-10-18
\| \| \| \| \| \| \|	Coqtop is not able to deal with broken states, hence Stm.interp has to immediately backtrack to the last meaningful state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
\| \| \| \| \| \| \| \|	Ideally, any component of the global state that is a function or any other unmarshallable data should be stocked as an ephemeron to make the state always marshallable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ephemeron: marshaling friendly keys	gareuselesinge	2013-10-18
\| \| \| \| \| \| \| \| \|	Ideally all unmarshallable content in the state should be stocked using Ephemeron keys. In this way the state becomes always marshallable (because the unmarshallable content is magically dropped). The mli contains more detailed doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Summary: if an unfreeze function fails, print an error message	gareuselesinge	2013-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
*	STM: not optimize proofs containing an Undo	gareuselesinge	2013-10-18
\| \| \| \| \| \| \|	Actually we could, but we should check the state one jumps to is inside the proof... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16889 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reintroduce "or" instead of "\|\|" as the latter is redifined in "sos_lib.ml" ↵	xclerc	2013-10-16
\| \| \| \| \| \|	with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Some more hand-written comparison functions to avoid polymorphic comparison.	xclerc	2013-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoid polymorphic comparison (plugins/rtauto).	xclerc	2013-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7