aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Collapse)AuthorAge
* ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDGravatar Pierre Letouzey2016-06-27
| | | | | | | | | The warnings were: Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND cpattern]. Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND lcpattern]. Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
| | | | Cf CHANGES for details.
* Removing tactic compatibility layers in setoid_ring.Gravatar Pierre-Marie Pédrot2016-06-24
|
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
| | | | | This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase.
* Fixing a mispelling coma -> comma.Gravatar Hugo Herbelin2016-06-16
|
* Adding printers for ring and field commands.Gravatar Hugo Herbelin2016-06-16
|
* Fixing printing of Function.Gravatar Hugo Herbelin2016-06-16
|
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* | Remove inappropriate comment.Gravatar Maxime Dénès2016-06-16
| |
| * Remove the syntax changes introduced by this branch.Gravatar Pierre-Marie Pédrot2016-06-15
| | | | | | | | | | | | We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6.
* | ssrmatching: giving proper credits to the original author(s)Gravatar Enrico Tassi2016-06-15
| | | | | | | | | | Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit.
* | ssrmatching: ltac argument parsing made more robustGravatar Enrico Tassi2016-06-15
| |
* | ssrmatching: debug prints sent via msg_debugGravatar Enrico Tassi2016-06-15
| |
* | Rename "Set SsrMatchingDebug" into "Set Debug SsrMatching"Gravatar Enrico Tassi2016-06-15
| | | | | | | | for uniformity with other Debug options.
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
| | | | | | | | | | | | | | The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument
* | port ssrmatching plugin to the new makefileGravatar Enrico Tassi2016-06-14
| |
* | Merge remote-tracking branch 'origin/pr/146' into trunkGravatar Enrico Tassi2016-06-14
|\ \ | | | | | | | | | | | | Conflicts: Makefile.common
* \ \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \ | | | | | | | | | | | | This is the "error resiliency" mode for STM
* \ \ \ Merge remote-tracking branch 'github/evarunsafe' into trunkGravatar Matthieu Sozeau2016-06-14
|\ \ \ \
| * | | | newring: fix for hack using evars as integers.Gravatar Matthieu Sozeau2016-06-09
| | | | |
* | | | | Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
* | | | Officially discontinue the experimental coq build via ocamlbuildGravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It has been accidentaly broken since early 2014 (and especially in 8.5), no easy repair, I won't devote any more hours to this stuff. Moreover no one seems to care apart from Emilio, but he's ok to work on this in a separate repository or branch. I left a dev/doc/ocamlbuild.txt file with a few words about this experiment.
| * | | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit introduces the concept of proof blocks that are resilient to errors. They are represented as ErrorBound boxes in the STM document with the topological invariant that they never overlap. The detection and error recovery of ErrorBound boxes is defined outside the STM. One can define a box by providing a function to detect it statically by crawling the parsed document and a function to recover from an error at run time.
* | | Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
| | | | | | | | | | | | | | | | | | Note that this breaks the compatibility, in a beneficial way I believe. Tactics defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction on a local identifier anymore. They must use the "fresh" primitive instead.
* | | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | functions about interpretation, internalization, externalization of notations. Main syntactic changes: - subst_aconstr_in_glob_constr -> instantiate_notation_constr (because aconstr has been renamed to notation_constr long time ago) - extern_symbol -> extern_notation (because symbol.ml has been renamed to notation.ml long time ago) - documentation of notations_ops.mli Main semantic changes: - Notation_ops.eq_glob_constr which was partial eq disappears: use glob_constr_eq instead - In particular, this impacts a change on funind which now use the (fully implemented) glob_constr_eq Somehow, instantiate_notation_constr should be in notation_ops.ml for symmetry with match_notation_constr but it is bit painful to do.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\ \ \
* | | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
| * | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| | | |
* | | | Extraction : add a location in the error message about polypropGravatar Pierre Letouzey2016-05-30
| | | |
| * | | Extraction/Projections: Fix bug #4710Gravatar Matthieu Sozeau2016-05-23
| | | | | | | | | | | | | | | | | | | | Use the compatibility match construction to extract the compatibility constant associated to a primitive projection.
| * | | Disable memoization rather than failing when files cannot be opened.Gravatar Guillaume Melquiond2016-05-20
| | | | | | | | | | | | | | | | | | | | Anomaly: Uncaught exception Unix.Unix_error(Unix.EACCES, "open", "lia.cache"). Please report.
* | | | Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
| | | |
| * | | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| | | |
* | | | Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
| | | |
* | | | Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new ↵Gravatar Pierre Letouzey2016-05-19
| | | | | | | | | | | | | | | | Init/Tauto.v)
* | | | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
| | | | | | | | | | | | | | | | | | | | | | | | It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead.
* | | | Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | | |
* | | | Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | | |
* | | | Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | | |
* | | | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
| | | |
* | | | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| | | |
* | | | Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
| | | |
* | | | More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
| | | |
* | | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
| | | |
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\| | |
| * | | Fix Haskell extraction for terms over 45 characters longGravatar Nickolai Zeldovich2016-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Haskell extraction code would allow line-wrapping of the Haskell type definition, which would lead to unparseable Haskell code when the linebreak occured just before the type name. In particular, with a term name of 46 characters or more, the following Coq code: Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt. Extraction Language Haskell. Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx. would produce: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :: Unit xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx = Tt which failed to compile with GHC (according to Haskell's indentation rules, the "Unit" line must be indented to be treated as a continuation of the previous line). This patch always forces the type onto a separate line, and ensures that it is always indented by 2 spaces (just like the body of each definition).
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 02:28:51 +0000