index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
cc
/
cctac.ml
Commit message (
Expand
)
Author
Age
*
Post-rebase warnings (unused opens and 2 unused values)
Gaetan Gilbert
2017-04-27
*
Removing tactic compatibility layer in congruence.
Pierre-Marie Pédrot
2017-04-24
*
Fix the API of the new pf_constr_of_global.
Pierre-Marie Pédrot
2017-04-24
*
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
*
Removing most nf_enter in tactics.
Pierre-Marie Pédrot
2017-02-14
*
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
Removing compatibility layers from Tacticals
Pierre-Marie Pédrot
2017-02-14
*
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
*
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
*
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
*
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
*
Cc API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
*
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tacmach API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
*
Typing API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Evarsolve API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
*
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
|
*
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
|
/
*
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-07
|
\
|
*
congruence: Restrict refreshing to Set
Matthieu Sozeau
2016-07-04
|
*
congruence: remove casts of indexed terms
Matthieu Sozeau
2016-07-04
|
*
congruence/univs: properly refresh (fix #4609)
Matthieu Sozeau
2016-07-04
*
|
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
|
|
*
Fixing a source of inefficiency and an artificial dependency in the
Daniel de Rauglaudre
2016-04-08
*
|
Using build_selector from Equality as a replacement of the selector
Hugo Herbelin
2016-03-05
*
|
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
\
*
|
|
Renaming functions in Typing to stick to the standard e_* scheme.
Pierre-Marie Pédrot
2016-02-15
|
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Merge remote-tracking branch 'origin/v8.5' into upstream-trunk
Hugo Herbelin
2015-11-07
|
\
|
|
*
Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan
Hugo Herbelin
2015-11-06
*
|
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
|
/
*
f_equal fix continued: do a refresh_universes as before.
Matthieu Sozeau
2015-10-08
*
Fix bug #4069: f_equal regression.
Matthieu Sozeau
2015-10-07
*
Univs: fix an evar leak in congruence
Matthieu Sozeau
2015-10-02
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
[next]