index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
CoqIDE: Add TAB key to autocomplete
ppedrot
2013-02-25
*
Fixing bug #2466
ppedrot
2013-02-24
*
New -no-native-compiler flag for configure, globally disabling the native
mdenes
2013-02-24
*
Reduced the noise level when dynlinking in bytecode mode or when
mdenes
2013-02-24
*
Tentative heuristic fix to handle lexer failures from CoqIDE when
ppedrot
2013-02-22
*
Cosmetic changes to CoqIDE finder widget.
ppedrot
2013-02-22
*
Names: con_modpath and con_label access back the user kn part
letouzey
2013-02-21
*
Added missing documentation of Set Printing Existential Instances.
herbelin
2013-02-21
*
A slightly more efficient test of well-typedness of restriction of
herbelin
2013-02-21
*
Added Evarsolve to the list of modules to open for debugging.
herbelin
2013-02-21
*
Fixing an annoying bug in CoqIDE which causes the very first line
ppedrot
2013-02-20
*
Fixing #2763
ppedrot
2013-02-20
*
More handling of scrollbars in CoqIDE completion
ppedrot
2013-02-20
*
CoqIDE: Including autocompletion in word proposals
ppedrot
2013-02-20
*
Corrects bug #2959 (error during Qed leads to assertion failure).
aspiwack
2013-02-20
*
Adding scrollbars to CoqIDE autocompletion
ppedrot
2013-02-20
*
New autocompletion mechanism in CoqIDE. Now provides many answers
ppedrot
2013-02-19
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
module_path --> ModPath.t, kernel_name --> KerName.t
letouzey
2013-02-19
*
Mod_subst: an extra assert
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Mod_subst: improve sharing during kn substitutions
letouzey
2013-02-18
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Adding more primitives to Exninfo
ppedrot
2013-02-18
*
Updating the backtrace handling mechanism to accomodate the new
ppedrot
2013-02-18
*
Added exception enrichment. Now one can define additional arbitrary
ppedrot
2013-02-18
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Extraction: same as commit 16203, hopefully without NotASort exns
letouzey
2013-02-18
*
Displaying environment and unfolding aliases in "cannot_unify"
herbelin
2013-02-17
*
A more informative message when the elimination predicate for
herbelin
2013-02-17
*
Locating errors from consider_remaining_unif_problems if possible
herbelin
2013-02-17
*
Added propagation of evars unification failure reasons for better
herbelin
2013-02-17
*
Revised the Ltac trace mechanism so that trace breaking due to
herbelin
2013-02-17
*
Fix extraction of inductive types that Coq auto-detects to be in Prop
letouzey
2013-02-14
*
CoqIDE: Adding escape reaction to replace widget
ppedrot
2013-02-13
*
Fixing autocompletion lock in CoqIDE
ppedrot
2013-02-13
*
make validate repaired via a temporary fix for #2949
letouzey
2013-02-13
*
Checker: re-sync vo structures after Maxime's commit 16136
letouzey
2013-02-12
*
Fixing bug in native compiler with let patterns in fixpoint definitions.
mdenes
2013-02-11
*
Useless use of hooks in VernacDefinition. In addition, this was
ppedrot
2013-02-10
*
Splitted Evarutil in two files
ppedrot
2013-02-10
*
Moved code from Pretype_error to Evarutil
ppedrot
2013-02-10
*
Revert "Ordered evars by level of dependency in the merging phase of unificat...
herbelin
2013-02-05
*
Fixed bug #2981 (anomaly NotASort in Retyping due to collision between
herbelin
2013-02-05
*
Fixing coqchk compilation after commit r16183
ppedrot
2013-02-03
*
v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)
herbelin
2013-02-01
*
Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).
herbelin
2013-01-29
[next]