aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
Commit message (Expand)AuthorAge
* Remove declare_object for SsrHave NoTCResolution.Gravatar Maxime Dénès2018-07-19
* Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
* Split the Ssrmatching module between code and grammar rules.Gravatar Pierre-Marie Pédrot2018-06-30
* Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorGravatar Maxime Dénès2018-06-25
|\
* \ Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \
| * | [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
| * | [ssr] simplify delayed clearsGravatar Enrico Tassi2018-06-22
* | | [ssr] set: merge universe constraints before type checking the termGravatar Enrico Tassi2018-06-22
|/ /
| * [ssr] rewrite: turn anomaly into regular errorGravatar Enrico Tassi2018-06-20
|/
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\
* \ Merge PR #7419: Remove 100 occurrences of Evd.emptyGravatar Pierre-Marie Pédrot2018-05-28
|\ \
| | * [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| |/ |/|
* | Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was addedGravatar Maxime Dénès2018-05-25
|\ \
| | * Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
| |/ |/|
* | Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
| * [ssr] fix after to_constr ~abort_on_undefined_evars was addedGravatar Enrico Tassi2018-05-16
* | Deprecate Refiner [evar_map ref] exported functions.Gravatar Gaëtan Gilbert2018-05-14
|/
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Merge PR #7237: [ssr] fix delayed clears (fix #7045)Gravatar Maxime Dénès2018-04-16
|\
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Gravatar Pierre-Marie Pédrot2018-04-13
|\ \
| | * [ssr] fix delayed clears (fix #7045)Gravatar Enrico Tassi2018-04-13
| |/ |/|
* | ssr: check cleared hyps do exist (fix #7050)Gravatar Enrico Tassi2018-04-04
| * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
|/
* Fix #7026: ssr: applying an overloaded lemma as a view takes too long.Gravatar Pierre-Marie Pédrot2018-03-21
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Maxime Dénès2018-03-08
|\ \
* \ \ Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\ \ \
* \ \ \ Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`Gravatar Maxime Dénès2018-03-07
|\ \ \ \
| | | | * Deprecate UState aliases in Evd.Gravatar Gaëtan Gilbert2018-03-06
| |_|_|/ |/| | |
* | | | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.Gravatar Maxime Dénès2018-03-06
|\ \ \ \
| | | | * ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Gravatar Enrico Tassi2018-03-06
* | | | | Merge PR #6896: [compat] Remove NOOP deprecated options.Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | | * Separate vim/emacs fold markers from ocamldoc commentsGravatar mrmr19932018-03-05
| |_|_|/ |/| | |
| | * | [ssreflect] Export parsing witnesses in mli file.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |/ / |/| |
* | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \
* \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \
| | | * | [compat] Remove NOOP and alias deprecated options.Gravatar Emilio Jesus Gallego Arias2018-03-04
| |_|/ / |/| | |
| | | * ssr: add Prenex Implicits for Some_inj to use it as a viewGravatar Anton Trunov2018-03-04
| | | * ssr: fix typo in doc commentGravatar Anton Trunov2018-03-04
| |_|/ |/| |
| * | ssr: ipats: V82.tactic ~nf_evars:false everywhereGravatar Enrico Tassi2018-03-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 11:27:42 +0000