Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: MetaCoq/metacoq
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: v1.3.2-8.20
Choose a base ref
...
head repository: MetaCoq/metacoq
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: coq-8.20
Choose a head ref
  • 10 commits
  • 18 files changed
  • 7 contributors

Commits on Sep 3, 2024

  1. Copy the full SHA
    f7f6ede View commit details
  2. Copy the full SHA
    b59ea92 View commit details

Commits on Oct 30, 2024

  1. Fix quoting and unquoting of primitive strings (#1109) for 8.29 (#1110)

    * initial fix
    
    * update test-suite
    
    Co-authored-by: MathisBD <75327344+MathisBD@users.noreply.github.com>
    yforster and MathisBD authored Oct 30, 2024
    Copy the full SHA
    f251f2a View commit details

Commits on Nov 22, 2024

  1. Copy the full SHA
    6e75b70 View commit details

Commits on Nov 25, 2024

  1. initial commit (#1122)

    Co-authored-by: Yannick Forster <yannick.forster@inria.fr>
    Co-authored-by: Théo Winterhalter <theo.winterhalter@inria.fr>
    3 people authored Nov 25, 2024
    Copy the full SHA
    5672294 View commit details

Commits on Dec 4, 2024

  1. Remove bugged option MetaCoq Template Monad Debug.

    It causes coq/vscoq#892 because `optwrite`
    is not supposed to be able to add persistent objects (libobject) to
    Coq's state but `set_option_value` does add one.
    
    It's also bugged as
    `set_option_value ~stage:Interp (fun _ v -> v) key i`
    sets the option to its current value not a new value.
    In other words `Set MetaCoq Template Monad Debug.` has no effect but
    its existence causes bugs.
    
    Since nobody complained about it not working it's not worth fixing it
    instead of deleting it (also I'm not sure it can be fixed with the
    currently available APIs).
    SkySkimmer authored and MathisBD committed Dec 4, 2024
    Copy the full SHA
    1fff46d View commit details
  2. Merge pull request #1126 from MathisBD/fix-bugged-option

    Remove bugged option MetaCoq Template Monad Debug.
    MathisBD authored Dec 4, 2024
    Copy the full SHA
    0b90e69 View commit details

Commits on Dec 30, 2024

  1. Copy the full SHA
    8d8a2fd View commit details
  2. update documentation

    MathisBD committed Dec 30, 2024
    Copy the full SHA
    9df908f View commit details
  3. Merge pull request #1131 from MathisBD/update-inductive-doc-8.20

    Update documentation in common/Environment.ml for inductive and constant declarations
    MathisBD authored Dec 30, 2024
    Copy the full SHA
    ea3ed3c View commit details
Loading