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
...
*
|
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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-07-02
*
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot
2015-02-27
[prev]