aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-02-20Adding scrollbars to CoqIDE autocompletionppedrot
2013-02-19New autocompletion mechanism in CoqIDE. Now provides many answersppedrot
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19module_path --> ModPath.t, kernel_name --> KerName.tletouzey
2013-02-19Mod_subst: an extra assertletouzey
2013-02-19Classops : avoid some use of Gmapletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-02-18Mod_subst: improve sharing during kn substitutionsletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18Adding more primitives to Exninfoppedrot
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-02-18Extraction: same as commit 16203, hopefully without NotASort exnsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 16:40:54 +0000