index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
auto_ind_decl.ml
Commit message (
Expand
)
Author
Age
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Bug 2636 - Move string_of_ppcmds to Pp
pboutill
2011-11-14
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Fixed "Scheme Equality" when another instance of the scheme on the
herbelin
2009-11-08
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
About "apply in":
herbelin
2008-12-09
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.
msozeau
2008-04-12
*
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
herbelin
2008-04-01
*
* Factorizing code : context_chop was used in several files (even as chop_con...
vsiles
2008-03-17
*
Nettoyage de code en vue de la release. Plus de Warning: Unused
aspiwack
2007-12-18
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-06
*
Added the automatic generation of the boolean equality if possible and the
vsiles
2007-10-05