index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
A slightly more efficient test of well-typedness of restriction of
herbelin
2013-02-21
*
avoid (Int.equal (cmp ...) 0) when a boolean equality exists
letouzey
2013-02-19
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Classops : avoid some use of Gmap
letouzey
2013-02-19
*
Removing Exc_located and using the new exception enrichement
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
*
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
*
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
*
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2013-01-29
*
Actually adding backtrace handling.
ppedrot
2013-01-28
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Fixing one part of #2830 (anomaly "defined twice" due to nested calls to
herbelin
2013-01-28
*
Added backtrace information to anomalies
ppedrot
2013-01-28
*
Ordered evars by level of dependency in the merging phase of unification
herbelin
2013-01-27
*
Improving formatting of output of "Test table".
herbelin
2013-01-27
*
Reductionops: whd_state_gen can take and answers a cst_stack too
pboutill
2013-01-24
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
- Fix evarconv so that we have complete eta-conversion:
msozeau
2013-01-22
*
Evarconv: Check stack before term in Canonical Structure approuval
pboutill
2013-01-18
*
Awful heuristic to refold mutual fixpoint in reductionops
pboutill
2012-12-21
*
Fixup and comment reductionops
pboutill
2012-12-21
*
Reductionops reduction machine can refold constant
pboutill
2012-12-19
*
Evarconv.Pseudorigid erasure
pboutill
2012-12-19
*
Array.create is deprecated
pboutill
2012-12-19
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Taking into account the possibility of having a type of type which is
herbelin
2012-12-18
*
Fixed a little inefficiency of "set/destruct" over a pattern. Now
herbelin
2012-12-18
*
Factorization of the elim unif flag with the default flag. Since
herbelin
2012-12-18
*
Do not display REVERTcast inserted by reduction tactics (unless printing all).
herbelin
2012-12-17
*
Fixed a bug in the algorithm trying to elaborate a "match" return predicate.
herbelin
2012-12-17
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Renamed Option.Misc.compare to the more uniform Option.equal.
ppedrot
2012-12-13
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Evarconv: Fix #2936 + comments
pboutill
2012-11-28
*
Reductionops uses Closure.reds
pboutill
2012-11-28
*
Removed some FIXME related to equality on universes.
ppedrot
2012-11-26
*
Small cleaning of interface in Univ
ppedrot
2012-11-26
*
More equality functions
ppedrot
2012-11-25
*
Fixed bug #2930: folded let-in's were hiding a violation to the occur
herbelin
2012-11-25
*
Added a constr_pattern_eq
ppedrot
2012-11-23
[next]