index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
termops.ml
Commit message (
Expand
)
Author
Age
*
Remove unused [open] statements
Gaetan Gilbert
2017-04-27
*
Remove some unused values and types
Gaetan Gilbert
2017-04-27
*
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
*
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
|
\
*
|
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
*
|
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
|
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
*
|
Removing some return type compatibility layers in Termops.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops 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
*
|
Rewrite API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Leminv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Inv API using EConstr.
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
*
|
Hipattern API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tacticals 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
*
|
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Cases API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Typeclasses API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Tacred API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Evarconv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-18
|
/
|
|
*
Fixes to compile with ocaml 4.01
Matthieu Sozeau
2016-11-07
*
|
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
|
Stronger static invariant in equality upto universes.
Pierre-Marie Pédrot
2016-10-31
*
|
Reordering Termops w.r.t. Evd and Namegen in engine folder.
Pierre-Marie Pédrot
2016-10-30
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-29
|
\
|
|
*
sections/hints: prevent Not_found in get_type_of
Matthieu Sozeau
2016-10-21
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-05
|
\
|
|
*
Tracking careless uses of slow name lookup.
Pierre-Marie Pédrot
2016-09-09
*
|
CLEANUP: using |> operator more consistently
Matej Kosik
2016-08-30
*
|
CLEANUP: removing "Termops.compact_named_context_reverse" function
Matej Kosik
2016-08-26
*
|
CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"
Matej Kosik
2016-08-26
*
|
CLEANUP: changing the definition of the "Context.NamedList.Declaration" type
Matej Kosik
2016-08-25
*
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Optmimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
*
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
API: documenting context_chop and removing a duplicate.
Hugo Herbelin
2015-12-15
*
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
*
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
[next]