Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Ported plugin to Coq 8.13 #43

Open
wants to merge 44 commits into
base: master
Choose a base branch
from
Open

Ported plugin to Coq 8.13 #43

wants to merge 44 commits into from

Commits on Jul 20, 2023

  1. Move build to dune.

    @agrarpan
    agrarpan committed Jul 20, 2023
    Configuration menu
    Copy the full SHA
    25b372f View commit details
    Browse the repository at this point in the history

  2. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 20, 2023
    Configuration menu
    Copy the full SHA
    60c6de8 View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2023

  1. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 21, 2023
    Configuration menu
    Copy the full SHA
    6e33a0a View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    1ac2061 View commit details
    Browse the repository at this point in the history

  2. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    816cdee View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2023

  1. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    858443e View commit details
    Browse the repository at this point in the history

  2. Fixed type errors, still some remaining.

    @agrarpan
    agrarpan committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    19e5b26 View commit details
    Browse the repository at this point in the history

  3. Undoing some changes from previous commit, using annotR uniformly now.

    @agrarpan
    agrarpan committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    7f0c7ec View commit details
    Browse the repository at this point in the history

Commits on Jul 27, 2023

  1. Change typo in .gitignore

    @agrarpan
    agrarpan committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    12f3ee5 View commit details
    Browse the repository at this point in the history

  2. Remove unsused function.

    @agrarpan
    agrarpan committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    1612ebc View commit details
    Browse the repository at this point in the history

  3. Renaming Globnames.global_reference to GlobRef.t

    @agrarpan
    agrarpan committed Jul 27, 2023
    Configuration menu
    Copy the full SHA
    d8a0d14 View commit details
    Browse the repository at this point in the history

Commits on Jul 28, 2023

  1. Fixed the type in indutils

    @agrarpan
    agrarpan committed Jul 28, 2023
    Configuration menu
    Copy the full SHA
    e3076e5 View commit details
    Browse the repository at this point in the history

Commits on Jul 31, 2023

  1. Fixed the type incompatibility in inference.ml

    @agrarpan
    agrarpan committed Jul 31, 2023
    Configuration menu
    Copy the full SHA
    0ebe46b View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2023

  1. Refactored to maintain the original semantics.

    @agrarpan
    agrarpan committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    fe44675 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2023

  1. Refactored constutils to handle type change of UnivGen.fresh_instance

    @agrarpan
    agrarpan committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    eadbabf View commit details
    Browse the repository at this point in the history

  2. Refactored indutils to handle type changes to Declarations.universes

    @agrarpan
    agrarpan committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    0b4e99f View commit details
    Browse the repository at this point in the history

  3. Refactored indutils to handle type changes to Declarations.universes

    @agrarpan
    agrarpan committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    b1064b3 View commit details
    Browse the repository at this point in the history

  4. Refactored defutils to handle type changes in Lemmas.hook_type

    @agrarpan
    agrarpan committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    43813af View commit details
    Browse the repository at this point in the history

  5. Added mlg file

    @agrarpan
    agrarpan committed Aug 7, 2023
    Configuration menu
    Copy the full SHA
    892b96c View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2023

  1. Merged changes from another fork branch to fix errors.

    @SkySkimmer @agrarpan
    SkySkimmer authored and agrarpan committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    7836367 View commit details
    Browse the repository at this point in the history

  2. Removed Makefile.local

    @agrarpan
    agrarpan committed Aug 8, 2023
    Configuration menu
    Copy the full SHA
    b3cd62c View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2023

  1. Renamed plugin to match template, builds with dune currently.

    @agrarpan
    agrarpan committed Aug 16, 2023
    Configuration menu
    Copy the full SHA
    55c3363 View commit details
    Browse the repository at this point in the history

Commits on Aug 18, 2023

  1. Fixed warnings.

    @agrarpan
    agrarpan committed Aug 18, 2023
    Configuration menu
    Copy the full SHA
    ffe7e16 View commit details
    Browse the repository at this point in the history

  2. Fixed warnings.

    @agrarpan
    agrarpan committed Aug 18, 2023
    Configuration menu
    Copy the full SHA
    b8af2c9 View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2023

  1. Added error handling for SProp.

    @agrarpan
    agrarpan committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    925fc08 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Changed the Context.binder_name usage to remove calls to annotR to ha… 

    …ndle SProp correctly.
    @agrarpan
    agrarpan committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    9e874d3 View commit details
    Browse the repository at this point in the history

  2. Changed the Context.binder_name usage to remove calls to annotR to ha… 

    …ndle SProp correctly.
    @agrarpan
    agrarpan committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    233f21d View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2023

  1. Filter out SProp eliminators based on string match for sind.

    @agrarpan
    agrarpan committed Oct 4, 2023
    Configuration menu
    Copy the full SHA
    7e47d4d View commit details
    Browse the repository at this point in the history

Commits on Oct 23, 2023

  1. Fixed bug that pushed the wrong name.

    @agrarpan
    agrarpan committed Oct 23, 2023
    Configuration menu
    Copy the full SHA
    525f61e View commit details
    Browse the repository at this point in the history

Commits on Oct 25, 2023

  1. Changed the arguments to declare_structure to reflect the API change.

    @agrarpan
    agrarpan committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    6607968 View commit details
    Browse the repository at this point in the history

  2. Filter out SProp sorts to prevent call to Indrec.lookup_eliminator.

    @agrarpan
    agrarpan committed Oct 25, 2023
    Configuration menu
    Copy the full SHA
    0082bd8 View commit details
    Browse the repository at this point in the history

Commits on Oct 26, 2023

  1. Pulled in Max's changes from 8.11 branch of coq-plugin-lib

    @agrarpan
    agrarpan committed Oct 26, 2023
    Configuration menu
    Copy the full SHA
    3a9de5d View commit details
    Browse the repository at this point in the history

Commits on Dec 4, 2023

  1. Made changes to the API to match Coq 8.12

    @agrarpan
    agrarpan committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    0921f90 View commit details
    Browse the repository at this point in the history

  2. Changed the cumulative flag to false to fix test errors in fix-to-elim

    @agrarpan
    agrarpan committed Dec 4, 2023
    Configuration menu
    Copy the full SHA
    9fd5b6f View commit details
    Browse the repository at this point in the history

Commits on Mar 27, 2024

  1. First attempt at fixing declare_definition bug.

    @agrarpan
    agrarpan committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    c1e4acd View commit details
    Browse the repository at this point in the history

  2. Passing false flag to EConstr.to_constr everywhere

    @agrarpan
    agrarpan committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    fc53570 View commit details
    Browse the repository at this point in the history

  3. Using declare_entry instead of declare_definition.

    @agrarpan
    agrarpan committed Mar 27, 2024
    Configuration menu
    Copy the full SHA
    f063181 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2024

  1. Remove undefined evars before calling declare_definition.

    @agrarpan
    agrarpan committed Apr 3, 2024
    Configuration menu
    Copy the full SHA
    603abcc View commit details
    Browse the repository at this point in the history

Commits on Apr 11, 2024

  1. Removed filter for sind.

    @agrarpan
    agrarpan committed Apr 11, 2024
    Configuration menu
    Copy the full SHA
    35de5ad View commit details
    Browse the repository at this point in the history

Commits on Apr 15, 2024

  1. First batch of changes for coq 8.13

    @agrarpan
    agrarpan committed Apr 15, 2024
    Configuration menu
    Copy the full SHA
    3ff1c96 View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2024

  1. Removed the refresh flag from the define_term and define_canonical in… 

    …terfaces since we dont use the results anyway.
    @agrarpan
    agrarpan committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    25774f7 View commit details
    Browse the repository at this point in the history

  2. Call Typing.type_of in case tyopt is not None.

    @agrarpan
    agrarpan committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    642f7ba View commit details
    Browse the repository at this point in the history

  3. Preserve original typing call.

    @agrarpan
    agrarpan committed Apr 30, 2024
    Configuration menu
    Copy the full SHA
    48a735a View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2024

  1. Update README.md

    @agrarpan
    agrarpan authored Jul 17, 2024
    Configuration menu
    Copy the full SHA
    7c7af85 View commit details
    Browse the repository at this point in the history