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
...
*
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
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
Cleaning and small optimization in CList.
ppedrot
2012-11-20
*
Added a CString module.
ppedrot
2012-11-13
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
Removing another bunch of generic equalities
ppedrot
2012-11-08
*
Reversed roles of undefined/defined evars in Evd, thus saving precious
ppedrot
2012-11-03
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
univ inconsistency error message gives evidence of a cycle
barras
2012-10-17
*
Adapt pieces of code needing -rectypes
letouzey
2012-10-06
*
Improving error message when abtraction over goal (abstract_list_all
herbelin
2012-10-04
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
More cleaning in CArray...
ppedrot
2012-09-18
[prev]
[next]