index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
reserve.ml
Commit message (
Expand
)
Author
Age
*
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-25
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Allows recursive patterns for binders to be associative on the left.
Hugo Herbelin
2018-02-20
*
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-22
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Better behaviour for sets of reserved names.
Pierre-Marie Pédrot
2014-03-01
*
Never suppress the typing constraint of bound variables whose name was
Pierre-Marie Pédrot
2014-03-01
*
Notations can now accept dummy arguments. If ever a bound variable is not
Pierre-Marie Pédrot
2013-12-22
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Replacing uses of association lists by maps in notations.
ppedrot
2013-08-03
*
Getting rid of module Gmapl.
ppedrot
2013-05-09
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (interp)
ppedrot
2012-11-25
*
More cleaning on Utils and CList. Some parts of the code being
ppedrot
2012-09-17
*
Some documentation and cleaning of CList and Util interfaces.
ppedrot
2012-09-15
*
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
*
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
*
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Fixing failing printer when the type of a binder name with implicit
herbelin
2011-10-24
*
Rather quick hack to avoid using notations involving "Type" when
herbelin
2011-06-12
*
Added a table for using reserved names for binding names to types
herbelin
2011-03-05
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Add information of localisation when an error involving an "implicit
herbelin
2010-11-07
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
[next]