aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.mli
AgeCommit message (Expand)Author
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-06-05Make direct invocations of `simple apply` obey `Opaque` directive.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-05-23unification.mli: Fix a spelling typo in a commentJason Gross
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Matthieu Sozeau
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-10-19More monotonicity in Tactics.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
2014-10-31Enlarge the cases where the like first selection is used in destruct.Hugo Herbelin
2014-10-26Fixing destruct/induction with a using clause on a non-inductive type,Hugo Herbelin
2014-10-25This commit introduces changes in induction and destruct.Hugo Herbelin
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-06-28Made the subterm finding function make_abstraction independent of theHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-05-30export Unification.abstract_list_all_with_dependenciespboutill
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-08-08Updating headers.herbelin
2011-12-17Added a flag to control the use of typing when instantiating appliedherbelin
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-04-18Add a flag to control betaiota reduction during unification to maintain backw...msozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2010-09-20Added eta-expansion in kernel, type inference and tactic unification,herbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:10:03 +0000