index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
rewrite.ml
Commit message (
Expand
)
Author
Age
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
*
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
*
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
Redo fix init_setoid -> init_relation_classes
Matthieu Sozeau
2016-03-09
*
Removing useless grammar.cma dependencies.
Pierre-Marie Pédrot
2016-03-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
Fixing bug #4596: [rewrite] broke in the past few weeks.
Pierre-Marie Pédrot
2016-02-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-21
|
\
|
|
*
Fix regression from 8.4 in reflexivity/...
Matthieu Sozeau
2016-02-19
|
*
Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity").
Pierre-Marie Pédrot
2016-02-17
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Using monotonic types for conversion functions.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Moving conversion functions to the new tactic API.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
*
|
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Implement support for universe binder lists in Instance and Program Fixpoint/...
Matthieu Sozeau
2016-01-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-13
|
\
|
*
|
CLEANUP: removing unused field
Matej Kosik
2016-01-11
|
*
Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.
Matthieu Sozeau
2016-01-11
|
*
Fix bug #4480: progress was not checked for setoid_rewrite.
Matthieu Sozeau
2016-01-07
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix in setoid_rewrite in Type: avoid the generation of a rigid universe
Matthieu Sozeau
2015-12-04
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-15
|
\
|
|
*
Continue fix of PMP, handling setoid_rewrite in let-bound hyps correctly.
Matthieu Sozeau
2015-11-13
|
*
Fix bug #3257, setoid_reflexivity should fail if not completing the goal.
Matthieu Sozeau
2015-11-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
|
\
|
|
*
Univs: local names handling.
Matthieu Sozeau
2015-10-28
*
|
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
|
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
|
Making Evarutil.new_evar monotonous.
Pierre-Marie Pédrot
2015-10-18
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
|
/
*
Fix some typos.
Guillaume Melquiond
2015-10-13
*
Remove code that was already commented out.
Maxime Dénès
2015-10-12
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
*
Hopefully better names to constructors of internal_flag, as discussed
Hugo Herbelin
2015-09-23
*
Fixing bug #4207: setoid_rewrite creates self-referring hypotheses.
Pierre-Marie Pédrot
2015-09-22
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
With the field record punning syntax.
Theo Zimmermann
2015-06-23
*
Put all arguments of strategy in record.
Theo Zimmermann
2015-06-23
*
Strategy is now a record type with a function field.
Theo Zimmermann
2015-06-23
*
Add comments.
Theo Zimmermann
2015-06-23
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Fixing bug #4232.
Pierre-Marie Pédrot
2015-05-11
*
Removing dead code in Rewrite.
Pierre-Marie Pédrot
2015-05-05
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Fix bug #3938
Matthieu Sozeau
2015-02-18
[next]