aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/evarutil.ml
Commit message (Expand)AuthorAge
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| |/
* / [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Moving evar-normalization functions to EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Making Evd independent from Namegen.Gravatar Pierre-Marie Pédrot2017-02-14
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\
| * Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-07
|\|
| * Fast path in push_rel_context_to_named_context.Gravatar Pierre-Marie Pédrot2016-09-05
| * Fast path in whd_evar.Gravatar Pierre-Marie Pédrot2016-09-02
* | Removing calls of "Context.Rel.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-26
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-26
* | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
|/
* Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
* Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
* Use sets instead of lists for names to avoid in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
* Simplifying code in evar generation.Gravatar Pierre-Marie Pédrot2016-08-04
* Exporting the renaming API for evar declaration.Gravatar Pierre-Marie Pédrot2016-08-04
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 08:25:29 +0000