index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
implicit_quantifiers.ml
Commit message (
Expand
)
Author
Age
*
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
*
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
*
Renaming local_binder into local_binder_expr.
Hugo Herbelin
2017-03-24
*
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-24
*
CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".
Matej Kosik
2016-10-19
*
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
*
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
|
*
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
*
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fixing bug #3811: "Universe annotations confused inside generalizing binders".
Pierre-Marie Pédrot
2015-07-29
*
Update headers.
Maxime Dénès
2015-01-12
*
Revert specific syntax for primitive projections, avoiding ugly
Matthieu Sozeau
2014-09-17
*
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
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...
letouzey
2013-03-12
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (interp)
ppedrot
2012-11-25
*
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
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Replacing some str with strbrk
ppedrot
2012-06-04
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
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
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Remove dynamic stuff from constr_expr and glob_constr
glondu
2011-10-28
*
Fixpoints are traverse during implicits arguments search to toplevel
pboutill
2011-02-10
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
Fix bug #2262: bad implicit argument number by avoiding counting
msozeau
2010-06-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Fix implicit_application for let-bound variables in the class context.
msozeau
2010-01-28
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Use generalizable variables info when internalizing arbitrary bindings,
msozeau
2009-11-08
[next]