index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
constrintern.ml
Commit message (
Expand
)
Author
Age
...
|
|
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
|
|
*
|
Using the same type of binders for interning and externing.
Hugo Herbelin
2017-03-24
|
|
*
|
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
|
|
*
|
Type extended_glob_local_binder now contains only glob_constr.
Hugo Herbelin
2017-03-24
|
|
*
|
Standardized the order of constructors for binders: Assum then Def.
Hugo Herbelin
2017-03-24
|
|
*
|
Cleaning phase around local binder at glob level:
Hugo Herbelin
2017-03-24
|
|
*
|
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-24
|
|
/
/
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-22
|
|
\
|
*
|
|
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
|
|
*
|
|
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
|
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
*
|
|
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
|
*
Fixing an anomaly with 'pat after cofix.
Hugo Herbelin
2017-02-02
|
*
|
Adding a new evar source to remember the name of evars which were
Hugo Herbelin
2017-01-22
|
/
/
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Fix #5048 - Casts in pattern raise an anomaly in Constrintern.
Maxime Dénès
2016-10-04
|
*
Quick fix to #4595 (making notations containing "ltac:" unused for printing).
Hugo Herbelin
2016-10-04
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
*
Fix bug #5087: Improve the error message on record with duplicated fields.
Pierre-Marie Pédrot
2016-10-02
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-23
|
\
|
|
*
typos
Enrico Tassi
2016-09-22
*
|
Revert "Merge remote-tracking branch 'github/pr/283' into trunk"
Maxime Dénès
2016-09-22
*
|
Merge remote-tracking branch 'github/pr/283' into trunk
Maxime Dénès
2016-09-22
|
\
\
*
|
|
Fix an error-prone error API.
Pierre-Marie Pédrot
2016-09-21
|
*
|
Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.
Maxime Dénès
2016-09-20
|
/
/
*
|
Generalizing the notion of constr substitution to generic arguments.
Pierre-Marie Pédrot
2016-09-15
*
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
|
|
/
|
/
|
*
|
Fix anomaly on user-inputted projection name (bug #5029).
Guillaume Melquiond
2016-08-19
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
Removing dead unsafe debugging code in Constrintern.
Pierre-Marie Pédrot
2016-08-16
*
Removing a source of clash with multiple recursive patterns in notations.
Hugo Herbelin
2016-07-19
*
Fixing #4932 (anomaly when using binders as terms in recursive notations).
Hugo Herbelin
2016-07-17
*
Fixing a collision about the meta-variable ".." in recursive notations.
Hugo Herbelin
2016-07-16
*
Merge remote-tracking branch 'github/bug4653' into v8.6
Matthieu Sozeau
2016-07-07
|
\
|
*
Do not use implicit type info for (x := t) bindings
Matthieu Sozeau
2016-07-07
*
|
Program: fix #4873: transparency option not used
Matthieu Sozeau
2016-07-07
|
*
Univs: fix internalization of (x := T) and casts
Matthieu Sozeau
2016-07-06
|
/
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2016-07-04
|
\
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
|
*
Univs: allowing notations to take univ instances
Matthieu Sozeau
2016-06-27
|
*
Forbidding silently dropped universes instances in
Matthieu Sozeau
2016-06-27
*
|
minor: comment on the meaning of the 'boolean' variable
Gabriel Scherer
2016-06-27
*
|
minor: documentation comment for constrintern.ml:sort_fields
Gabriel Scherer
2016-06-27
*
|
minor: interp/constrintern.ml, clarify field completion
Gabriel Scherer
2016-06-27
*
|
minor: in constrintern.ml:sort_fields, clarify sf
Gabriel Scherer
2016-06-27
*
|
minor: in constrintern.ml:sort_fields, clarify build_patt
Gabriel Scherer
2016-06-27
[prev]
[next]