aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-03-30ocamlformat: use whitelist instead of blacklistGaëtan Gilbert
Using disable=true in .ocamlformat and disable=false in sub .ocamlformat works fine. Note that disable=true must be after the `profile` setting otherwise it gets reset
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
Reviewed-by: herbelin
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
There is not need to re-export Gramlib's API in a non-structured way anymore. We thus expose the core Gramlib interface to users and remove redundant functions. A question about whether to move more parts of the API to `Gramlib` is still open, as well as on naming.
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
We remove Coq's wrapper over gramlib's grammar constructors.
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
After the gramlib merge and the type-safe interface added to it, the grammar extension type is redundant; we thus make it private as a first step on consolidating it with the one in gramlib's.
2020-03-25[ocamlformat] Use doc-comments=before style.Emilio Jesus Gallego Arias
IMHO it is a bit more logical, WDYT?
2020-03-25Nicer printing for decimal constants in RPierre Roux
Print 1.5 as 1.5 and not 15e-1. We choose the shortest representation with tie break to the dot notation (0.01 rather than 1e-3). The printing remains injective, i.e. 12*10^2 is printed 12e2 in order not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the first being printed as 1.2 and the last as 1.20.
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
Warning: in notations, the name "bigint" actually meant "bignat". A clarification will eventually be needed.
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
Reviewed-by: Matafou
2020-03-20Merge PR #11857: Remove calls to structural equality in MicromegaVincent Laporte
Reviewed-by: vbgl
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
Most of the parameters were named, we fix the remaining cases.
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
- Legacy attributes can now be specified in any order. - Legacy attribute Cumulative maps to universes(cumulative). - Legacy attribute NonCumulative maps to universes(noncumulative). - Legacy attribute Private maps to private(matching). We use "private(matching)" and not "private(match)" because we cannot use keywords within attributes.
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Fuck off ocamlformat.Pierre-Marie Pédrot
2020-03-19Reduce the scope of a call to pervasive equality in Coq_micromega.Pierre-Marie Pédrot
2020-03-19Use monomorphic comparison functions in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Dedicate type for monomials in Micromega.Vect.Pierre-Marie Pédrot
This enforces monomorphism everywhere possible.
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
We reuse the same type as for options, even though it is a bit ill-named. At least it allows to share code with it.
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind.
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
Fixes #11846: Funind fails to generate principles for terms with let bindings.
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
Since tclOR/tclORELSE are not supposed to return critical exceptions, we don't need to replace catchable_exception by noncritical.
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-11Merge PR #11754: [micromega] Add numerical compatibility layer.Frédéric Besson
Ack-by: SkySkimmer Reviewed-by: fajb
2020-03-11Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-10Merge PR #11767: Fix #11738 : Funind using deprecated Coqlib API.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-10[plugins] [cc] Remove unused exports / mli file cleanup.Emilio Jesus Gallego Arias
2020-03-10[clib] Remove module CStackEmilio Jesus Gallego Arias
This is only used in `Ccalgo` and it does not provide any advantage these days over the upstream OCaml implementation.
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ↵Pierre-Marie Pédrot
following the model of `pose (x:=t)`. Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-04[micromega] Add numerical compatibility layer.Emilio Jesus Gallego Arias
Only significant change is in gcd / lcm which now are typed in `Z.t`
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
Reviewed-by: vbgl
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
Reviewed-by: Matafou Reviewed-by: ppedrot
2020-03-04Merge PR #11709: Deprecate the "prolog" tactic.Théo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 18:11:11 +0000