index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
quote
Commit message (
Expand
)
Author
Age
*
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
*
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Pierre-Marie Pédrot
2016-09-15
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Compilation via pack for plugins of the stdlib
Pierre Letouzey
2016-06-08
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
The tactic generic argument now returns a value rather than a glob_expr.
Pierre-Marie Pédrot
2016-02-22
*
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
2015-11-20
|
\
|
|
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
*
|
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
|
/
*
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-03-03
*
Update headers.
Maxime Dénès
2015-01-12
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
A version of convert_concl and convert_hyp in new proof engine.
Hugo Herbelin
2014-10-09
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
Matthieu Sozeau
2014-08-25
*
Now parsing rules of ML-declared tactics are only made available after the
Pierre-Marie Pédrot
2014-05-12
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
Pierre Letouzey
2014-03-02
*
Do not use ugly Dyn features in the Quote plugin. Use instead the
Pierre-Marie Pédrot
2013-11-26
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Replacing lists by maps in matching interpretation.
ppedrot
2013-06-05
*
Restrict (try...with...) to avoid catching critical exn (part 7)
letouzey
2013-03-13
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of identifier
ppedrot
2012-12-14
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
place all files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29
*
Pattern as a mli-only file, operations in Patternops
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Quote: replaced various generic = on constr by eq_constr, destructors etc.
puech
2011-07-29
*
Quote: replaced generic = on constr by eq_constr
puech
2011-07-29
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
More {raw => glob} changes for consistency
glondu
2010-12-24
[next]