Code

[TC] HO unification#571

Code

Closed

FissoreD wants to merge 81 commits intoLPCIC:masterLPCIC/coq-elpi:masterfrom FissoreD:pglobal1FissoreD/coq-elpi:pglobal1Copy head branch name to clipboard

+1,769-422

Commits

Commits on Jan 8, 2024

• compile pglobal instances

  Show description for e1f4964
  FissoreD

  committed
  e1f4964

• Update tests

  FissoreD

  committed
  cb673e5

• WIP

  FissoreD

  committed
  16b1aac

• restore coq-elpi-builtins

  FissoreD

  committed
  f85a894

• avoid declaring option twice

  FissoreD

  committed
  db36d07

Commits on Jan 9, 2024

• fix Elpi Typecheck program

  gares

  committed
  bb3fbb7

• wip: hook for default instances

  gares

  committed
  9ca7dd1

• unify-FO heuristic

  gares

  committed
  c1e46dc

• spec for HO cases

  gares

  committed
  3cf1aee

• silence

  gares

  committed
  5daf079

• refactor

  gares

  committed
  8ec9dd6

• HO support

  gares

  committed
  baedca2

• nicer error

  gares

  committed
  7f8a26d

• wip

  gares

  committed
  24336f9

• Custom rules for eta-contraction in goal and sub-goals

  Show description for 65e73ea
  FissoreD

  committed
  65e73ea

• Command TC.Unfold to reason with alias (eg Nat.succ and S)

  FissoreD

  committed
  21dfec5

• some comments in create_tc_predicate

  FissoreD

  committed
  1cdb613

Commits on Jan 10, 2024

• Term of correct type in HO unif with multiple lambdas

  FissoreD

  committed
  8ed4dae

• fix the other eta contract

  gares

  committed
  b0bc947

• HO premises in their natural order

  gares

  committed
  d268f7b

• minor changes

  FissoreD

  committed
  40e6458

• typo

  FissoreD

  committed
  fdd356c

• hide of warning

  FissoreD

  committed
  481470c

• class with coercion in field

  FissoreD

  committed
  54b0b80

Commits on Jan 11, 2024

• silence warning

  gares

  committed
  124dc0f

• fix unfold (you need beta)

  gares

  committed
  ac6aa08

Commits on Jan 12, 2024

• a search fail raises a ltac.fail instead of a fatal error

  

  FissoreD

  authored and

  gares

  committed
  474b317

• solve_TC good behavior on LtacFail

  

  FissoreD

  authored and

  gares

  committed
  e1e8180

• is_available_option_name function

  FissoreD

  committed
  390911d

Commits on Jan 14, 2024

• Incorrectly compiled coercion instances are removed

  FissoreD

  committed
  e0c7109

• small fix

  FissoreD

  committed
  32c03f7

• Elpi Typeclasses Debug command to print coq search

  FissoreD

  committed
  bcb1a68

• vscoq anomaly TC.Compiler already register replaced with warning

  FissoreD

  committed
  80a438b

• msg_debug -> msg_warning

  FissoreD

  committed
  dc75009

Commits on Jan 15, 2024

• Replace api

  FissoreD

  committed
  be93226

• wip

  gares

  committed
  a5871fb

• wip-ho

  gares

  committed
  9a0e4d9

• wip-ho

  gares

  committed
  87f78c3

• sketch

  gares

  committed
  0a5d611

• Remove trivial debug message

  FissoreD

  committed
  b2f6149

• remove useless predicate

  FissoreD

  committed
  e024447

Commits on Jan 16, 2024

• clause for eta-contract is generated

  FissoreD

  committed
  e4076d6

• ho pred in a separate file

  FissoreD

  committed
  a2f3e7b

• clean solver.elpi

  FissoreD

  committed
  30ec1a5

• clean compiler.elpi

  FissoreD

  committed
  b393382

• OK: solve PF if in goal

  FissoreD

  committed
  b3a573a

• rework dependencies

  FissoreD

  committed
  6368513

• add of std.do!

  FissoreD

  committed
  298282d

• ho-link correction

  FissoreD

  committed
  1c521ee

Commits on Jan 18, 2024

• HO unif progress

  FissoreD

  committed
  974c07f

• Merge branches of compile-aux

  FissoreD

  committed
  518a11d

• todo

  FissoreD

  committed
  8977181

Commits on Jan 19, 2024

• wip

  FissoreD

  committed
  f26fd0a

• works

  FissoreD

  committed
  dc372ca

• works

  FissoreD

  committed
  d1773aa

• works

  FissoreD

  committed
  a4a8b53

• works

  FissoreD

  committed
  df90747

• really works

  FissoreD

  committed
  be4c521

• kont 0

  FissoreD

  committed
  e98b7a4

• kont 0

  FissoreD

  committed
  926dcaf

• nice

  FissoreD

  committed
  855275b

• nice

  FissoreD

  committed
  a301ab0

• nice

  FissoreD

  committed
  91efc5d

• nice

  FissoreD

  committed
  21a2988

Commits on Jan 23, 2024

• wip

  FissoreD

  committed
  d8947c5

• Add TC.Pending_mode command

  FissoreD

  committed
  7eefcdf

• Check pending mode arity

  FissoreD

  committed
  c2bb1cb

Commits on Jan 24, 2024

• Modes stored in class predicate

  FissoreD

  committed
  bf156de

• small refactor

  FissoreD

  committed
  5ab3839

• code clean

  FissoreD

  committed
  cbe7639

• align modes

  FissoreD

  committed
  1619ffa

• wip

  FissoreD

  committed
  6d6bae6

Commits on Jan 25, 2024

• trace_browser file name with unixgettimeofday

  FissoreD

  committed
  f117890

• declare-evar does nothing on evar in goal

  FissoreD

  committed
  10dcb49

• wip

  FissoreD

  committed
  1484813

Commits on Jan 26, 2024

• Revert "align modes"

  Show description for a70197b
  FissoreD

  committed
  a70197b

• Clean solver.elpi

  FissoreD

  committed
  e97c291

Commits on Jan 27, 2024

• change error msg when section var are cleared

  FissoreD

  committed
  4524b55

Commits on Feb 6, 2024

• more comments + declare-evar-later

  FissoreD

  committed
  3426c86

Commits on Feb 14, 2024

• Remove accumulate in elpi file to avoid rule duplication

  FissoreD

  committed
  8f9558f

Commits on Feb 15, 2024

• some comments

  FissoreD

  committed
  aff8ae9