index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
glob_ops.ml
Commit message (
Expand
)
Author
Age
*
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-18
*
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Hugo Herbelin
2016-07-17
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Fixing #4677 (collision of a global variable and of a local variable
Hugo Herbelin
2016-04-19
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
Fixing obviously untested fold_glob_constr and iter_glob_constr.
Hugo Herbelin
2015-10-11
*
Update headers.
Maxime Dénès
2015-01-12
*
Printing function for [uconstr].
Arnaud Spiwack
2014-11-19
*
Glob-ops: a name-mapping operation for pattern-matching binders.
Arnaud Spiwack
2014-11-19
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Adding an equality function over glob_constr
Pierre-Marie Pédrot
2014-03-02
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Added a constr_pattern_eq
ppedrot
2012-11-23
*
Monomorphization (pretyping)
ppedrot
2012-11-22
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29