aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* Merge PR #6496: Generate typed generic code from ltac macrosGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ | | | | | | | | | wish #4129)
* \ \ Merge PR #6893: Cleanup UState API usageGravatar Maxime Dénès2018-03-08
|\ \ \
| | | * Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | Today, TACTIC EXTEND generates ad-hoc ML code that registers the tactic and its parsing rule. Instead, we make it generate a typed AST that is passed to the parser and a generic tactic execution routine. PMP has written a small parser that can generate the same typed ASTs without relying on camlp5, which is overkill for such simple macros.
* | | Merge PR #6918: romega: get rid of EConstr.UnsafeGravatar Maxime Dénès2018-03-08
|\ \ \
* \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6934: Warn when using “Require” in a sectionGravatar 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
|\ \ \ \ \ \
| | * | | | | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6932: [stdlib] Do not use deprecated notationsGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \
* \ \ \ \ \ \ 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
|\ \ \ \ \ \ \ \
| | | | | | | | * An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
| | | | | | | | * Extraction: switch to EConstr.t as the central type to extract from.Gravatar Pierre Letouzey2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a bit artificial since the extraction normally operates on finished constrs (with no evars). But: - Since we use Retyping quite a lot, switching to EConstr.t allows to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))` - This prepares the way for a possible extraction of the content of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
| | | | | | * | | romega: get rid of EConstr.UnsafeGravatar Pierre Letouzey2018-03-06
| | | | | | | |/ | | | | | | |/| | | | | | | | | | | | | | | | | We replace constr by EConstr.t everywhere, and propagate some extra sigma args
| | | * | | / | [stdlib] Do not use deprecated notationsGravatar Vincent Laporte2018-03-06
| |_|/ / / / / |/| | | | | |
| | | | | | * Rename some universe minimizing "normalize" functions to "minimize"Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | UState normalize -> minimize, Evd nf_constraints -> minimize_universes
| | | | | | * 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
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"Gravatar Maxime Dénès2018-03-06
|\ \ \ \ \ \ \ \ | |_|_|_|_|/ / / |/| | | | | | |
| | | | | * | | Escape curly braces in ocamldoc commentGravatar mrmr19932018-03-05
| | | | | | | |
| | | | | * | | Separate vim/emacs fold markers from ocamldoc commentsGravatar mrmr19932018-03-05
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | ocamldoc chokes on the markers {{{ and }}} because { and } are part of its syntax
| | | * | | | [ssreflect] Export parsing witnesses in mli file.Gravatar Emilio Jesus Gallego Arias2018-03-05
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
* | | | | | 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
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
| | | | * | | 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
| | | | | |
| * | | | | ssr: rewrite Ssripats and Ssrview in the tactic monadGravatar Enrico Tassi2018-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
* | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
* | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | coretactics.ml4.
* \ \ \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ |/| | | | | | |
| | | | | | | * Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-03-04
| |_|_|_|_|_|/ |/| | | | | |
| | | | | | * [compat] Remove "Intuition Iff Unfolding"Gravatar Emilio Jesus Gallego Arias2018-03-03
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | Following up on #6791, we remove the option "Intuition Iff Unfolding"
| | | | * | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
| |_|_|/ / |/| | | | | | | | | | | | | | Fix new deprecation warnings in the standard library.
| | * | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| |/ / / |/| | |
| | * | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
* | | Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ↵Gravatar Maxime Dénès2018-02-28
|\ \ \ | | | | | | | | | | | | Ring_theory.v)
| | | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ |/| |
* | | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \
* \ \ \ Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \ \ \
| | | | * proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
| | | | |
| | | * | Fixes #6787 (minus sign interpreted by coqdoc as a bullet in Ring_theory.v).Gravatar Hugo Herbelin2018-02-20
| | | |/
* | | | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | Renaming it register_grammars_by_name.
* | | | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 19:37:10 +0000