aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-02-17Displaying environment and unfolding aliases in "cannot_unify"herbelin
2013-02-17A more informative message when the elimination predicate forherbelin
2013-02-17Locating errors from consider_remaining_unif_problems if possibleherbelin
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-02-14Fix extraction of inductive types that Coq auto-detects to be in Propletouzey
2013-02-13CoqIDE: Adding escape reaction to replace widgetppedrot
2013-02-13Fixing autocompletion lock in CoqIDEppedrot
2013-02-13make validate repaired via a temporary fix for #2949letouzey
2013-02-12Checker: re-sync vo structures after Maxime's commit 16136letouzey
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2013-02-10Splitted Evarutil in two filesppedrot
2013-02-10Moved code from Pretype_error to Evarutilppedrot
2013-02-05Revert "Ordered evars by level of dependency in the merging phase of unificat...herbelin
2013-02-05Fixed bug #2981 (anomaly NotASort in Retyping due to collision betweenherbelin
2013-02-03Fixing coqchk compilation after commit r16183ppedrot
2013-02-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
2013-01-29Added a file for testing regression of bug #2955 (anomaly in simpl inherbelin
2013-01-29No reason a priori for using unfiltered env for printingherbelin
2013-01-29Fixing bug #2969 (admit failing after Grab Existential Variables dueherbelin
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Added backtrace primitives.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Fixing one part of #2830 (anomaly "defined twice" due to nested calls toherbelin
2013-01-28native_compute: Fixed dependencies compilation order.mdenes
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-27Ordered evars by level of dependency in the merging phase of unificationherbelin
2013-01-27Improving formatting of output of "Test table".herbelin
2013-01-27Fixed bug #2967 (some missing check on ill-formed recursive notation strings).herbelin
2013-01-27Slightly improving some debugging printing and error message for modules.herbelin
2013-01-27Avoid failure in debugger when printing Ltac names.herbelin
2013-01-26updating ide/coq documentationppedrot
2013-01-26Monadification of coqtop queries in CoqIDEppedrot
2013-01-26Uniformization of Coq tasksppedrot
2013-01-25Better handling of escape find in CoqIDEppedrot
2013-01-25Better Undo/Redo mechanismppedrot
2013-01-25Trying to fix CoqIDE undo/redo mechanismppedrot
2013-01-25Fixing autocompletion in CoqIDEppedrot
2013-01-25Fixup last commitppedrot
2013-01-25Hugo request: CoqIDE find on enterppedrot
2013-01-24Reductionops: whd_state_gen can take and answers a cst_stack toopboutill
2013-01-24Fixed parsing of -no-native-compiler flag.mdenes
2013-01-24Native compiler: warnings were not turned off for OCaml 3.11mdenes
2013-01-23Coqide: limit read buffer size to 4096 (pipe size in win32)letouzey
2013-01-22Coqide: avoid potentially blocking read on coqtop channelletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:51:19 +0000