coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix ambiguous regex in syntax highlighting.	Guillaume Melquiond	2014-09-17
\| \| \| \| \| \| \|	This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them.
*	Change an axiom into a definition.	Guillaume Melquiond	2014-09-17
\|
*	Fix broken syntax highlighting for Coq files using "Proof constr".	Guillaume Melquiond	2014-09-17
\| \| \| \| \| \|	See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof.
*	win32: bring back the coq icon in the coqide binary	Enrico Tassi	2014-09-17
\|
*	win32: use subsystem windows on windows (and not console)	Enrico Tassi	2014-09-17
\| \| \| \|	This makes the hammer tools/mkwinapp.ml kind of obsolete
*	Revert "While resolving typeclass evars in clenv, touch only the ones that ↵	Matthieu Sozeau	2014-09-17
\| \| \| \| \| \| \| \|	appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
*	While resolving typeclass evars in clenv, touch only the ones that appear in the	Matthieu Sozeau	2014-09-17
\| \| \| \| \|	clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633).
*	Update test-suite files after last commit. Add a file for rewrite_strat	Matthieu Sozeau	2014-09-17
\| \| \| \|	examples.
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
\| \| \| \| \| \| \| \|	contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
*	Undo prints only if coqtop \|\| emacs	Enrico Tassi	2014-09-16
\|
*	better error message	Enrico Tassi	2014-09-16
\|
*	fix test-suite/success/decl_mode.v	Enrico Tassi	2014-09-16
\|
*	More on printing references applied to implicit arguments.	Hugo Herbelin	2014-09-16
\|
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \|	of resulution for goals whose head is "ref". + means the argument is an input and shouldn't contain an evar, otherwise resolution fails. This generalizes the Typeclasses Strict Resolution option which prevents resolution to fire on underconstrained typeclass constraints, now the criterion can be applied to specific parameters. Also cleanup auto/eauto code, uncovering a potential backwards compatibility issue: in cases the goal contains existentials, we never use the discrimination net in auto/eauto. We should try to set this on once the contribs are stabilized (the stdlib goes through when the dnet is used in these cases).
*	Adapting ltac output test to new interpretation of binders.	Hugo Herbelin	2014-09-15
\|
*	Fixing printing of @eq which was apparently wrong bug fixed by MS on Wed 10.	Hugo Herbelin	2014-09-15
\|
*	Not printing goal name (reinstalled by mistake in a previous commit).	Hugo Herbelin	2014-09-15
\|
*	Fixing line break in test for #3559.	Hugo Herbelin	2014-09-15
\|
*	Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].	Arnaud Spiwack	2014-09-15
\| \| \| \|	All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
*	Ltac names in binders: some Ltac values can be seen both as terms and ↵	Arnaud Spiwack	2014-09-15
\| \| \| \| \|	identifiers. Fixes Ergo.
*	Fix: when interpreting a identifier in pretying, use the Ltac identifier ↵	Arnaud Spiwack	2014-09-15
\| \| \| \| \|	substitution at the right place. I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
*	Fix a bug in the naming of binders.	Arnaud Spiwack	2014-09-15
\| \| \|	The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
*	A small pass of code cleaning and clenv removing in Rewrite.	Pierre-Marie Pédrot	2014-09-15
\|
*	Fixing bug #3619 in emacs mode.	Hugo Herbelin	2014-09-15
\|
*	Avoid backtracking in typeclass search if a solution for a closed	Matthieu Sozeau	2014-09-15
\| \| \| \| \|	non-dependent or propositional constraint has already been found (same behavior as before previous patch).
*	Fix bug #3610, allowing betaiotadelta reduction while unifying types of	Matthieu Sozeau	2014-09-15
\| \| \| \|	records in unification.ml.
*	Fix bug #3621, using fold_left2 on arrays of the same size only.	Matthieu Sozeau	2014-09-15
\|
*	Rework typeclass resolution and control of backtracking.	Matthieu Sozeau	2014-09-15
\| \| \| \| \| \| \|	Add a global option to check for multiple solutions and fail in that case. Add another flag to declare classes as having unique instances (not checked but assumed correct, avoiding some backtracking).
*	Removing one Evd.merge in Rewrite.	Pierre-Marie Pédrot	2014-09-15
\|
*	More invariants in Rewrite unification.	Pierre-Marie Pédrot	2014-09-15
\|
*	The unifying functions of Rewrite uses the return types of strategies.	Pierre-Marie Pédrot	2014-09-15
\|
*	Splitting the uses of the unification function according to the status of	Pierre-Marie Pédrot	2014-09-15
\| \| \| \|	the abs flag in rewrite.
*	Rewrite.apply_strategy uses the same return type as strategies.	Pierre-Marie Pédrot	2014-09-14
\|
*	Proper type for rewrite strategy results.	Pierre-Marie Pédrot	2014-09-14
\|
*	Prepare goal name printing but no not print them at the current time.	Hugo Herbelin	2014-09-13
\|
*	Using "Evd.restrict" in tactic clear so as to keep evar names.	Hugo Herbelin	2014-09-13
\|
*	Exporting apply_subfilter from Evd.ml.	Hugo Herbelin	2014-09-13
\|
*	Retroknowledge arguments are made VERNAC ARGUMENTS.	Pierre-Marie Pédrot	2014-09-13
\|
*	Fixing synchronization of evar names table when merging evar_map.	Hugo Herbelin	2014-09-13
\|
*	Providing a -type-in-type option for collapsing the universe hierarchy.	Hugo Herbelin	2014-09-13
\|
*	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin	2014-09-13
\| \| \| \|	in instances.
*	Fixing injection bug #3616 on sigma-types.	Hugo Herbelin	2014-09-13
\|
*	While we don't have a clean alternative to Clenvtac, add a primitive	Matthieu Sozeau	2014-09-12
\| \| \| \|	for tclEVARS which might solve existing goals.
*	Fix base_include due to change in argument order of env and evar_map	Matthieu Sozeau	2014-09-12
\|
*	An old typo which was preventing example #3537 to work the same as it	Hugo Herbelin	2014-09-12
\| \| \| \|	was working in 8.4.
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
\|
*	Use evar name to print goal.	Hugo Herbelin	2014-09-12
\|
*	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin	2014-09-12
\|
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
\|
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
\| \| \| \| \|	instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.