index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
tacred.ml
Commit message (
Expand
)
Author
Age
...
*
Updating headers.
herbelin
2012-08-08
*
Reductionops refactoring
pboutill
2012-07-20
*
Fixing test-suite
pboutill
2012-07-20
*
tacred uses stack_reduction_function instead of state_reduction_function
pboutill
2012-07-12
*
Reductionops : Better abstract machine stack utilities
pboutill
2012-06-15
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Pattern as a mli-only file, operations in Patternops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Fixes bug: #2692 (Arguments/simpl off by 1)
gareuselesinge
2012-03-19
*
Arguments/simpl: allow ! even on non fixpoints
gareuselesinge
2012-03-19
*
Noise for nothing
pboutill
2012-03-02
*
Bug #2041: unfold at betaiotaZETA normalize like unfold
pboutill
2012-01-31
*
Granted legitimate wish #2607 (not exposing crude fixpoint body of
herbelin
2011-12-18
*
Configurable simpl tactic
gareuselesinge
2011-11-21
*
Generalizing subst_term_occ so that it supports an arbitrary matching
herbelin
2011-09-26
*
Tacred: generic equality on constr replaced by eq_constr
puech
2011-07-29
*
Make simpl use the proper constant when folding (mutual) fixpoints
letouzey
2011-01-27
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Slight cosmetic cleaning of tacred.ml.
herbelin
2010-10-31
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
herbelin
2009-08-07
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Fixed bug #2116 ("simpl" created ill-typed term while accepting
herbelin
2009-07-08
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
pushed evar reduction in kernel
barras
2009-02-06
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
improved simpl
barras
2008-12-03
*
another bug with simpl
barras
2008-11-28
*
fixed bug 1791: simpl was performing eta expansion
barras
2008-11-27
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
refined the conversion oracle
barras
2008-05-21
*
Correction bug 1835 + correction bug occur-check résultant en un
herbelin
2008-04-18
*
fold travaille maintenant sur la forme beta-iota-zeta réduite du
herbelin
2008-03-10
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Petit complément au commit 10131.
herbelin
2007-09-21
*
- Fixing bug 1703 ("intros until n" falls back on the variable name when
herbelin
2007-09-21
*
Protection d'un warning par if_verbose
herbelin
2007-05-21
*
Suite du commit 9760 : l'uniformisation du comportement de one_step_reduce,
herbelin
2007-04-14
*
Correction bug #1491
herbelin
2007-04-13
[prev]
[next]