aboutsummaryrefslogtreecommitdiff
path: root/proofs/evar_refiner.ml
AgeCommit message (Expand)Author
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
2019-02-05Make Program a regular attributeMaxime Dénès
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-16Remove the implicit tactic feature following #7229.Pierre-Marie Pédrot
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-08-01Move glob_constr_ltac_closure to evar_refiner.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-13Fixing printing of evar name in an error message of instantiate.Hugo Herbelin
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-03-20Extruding the code for the Existential command from Proofview.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-07Better structure for Ltac pretyping environments.Pierre-Marie Pédrot
2014-08-06[uconstr]: use a closure instead of eager substitution.Arnaud Spiwack
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 12)letouzey
2013-02-17Added propagation of evars unification failure reasons for betterherbelin
2013-01-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
2012-11-25Monomorphization (proof)ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:42:36 +0000