aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.mli
Commit message (Expand)AuthorAge
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
* Fix canonical structure resolution which was launched on the results ofGravatar Matthieu Sozeau2014-09-26
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* Cst_stack before stack (abstraction leak in whd_gen)Gravatar Pierre Boutillier2014-05-26
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fixes for canonical structure resolution (check that the initial term indee...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* consider_remaining_unif_problems respects Conv_oracleGravatar Pierre Boutillier2014-03-16
* Evarconv unification respects Conv_oracleGravatar Pierre Boutillier2014-03-10
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* comments in mliGravatar pboutill2013-05-30
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* A few comments in evarconv.mli.Gravatar herbelin2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo...Gravatar pboutill2013-02-25
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
* Updating headers.Gravatar herbelin2012-08-08
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Refined second_order_matching so that a constraint on whichGravatar herbelin2011-11-08
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* Applied the trick of Chung-Kil Hur to solve second-order matchingGravatar herbelin2011-10-10
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fix treatment of remaining unification constraints: raise a moreGravatar msozeau2010-03-07
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17