From 1c9e1a39652b401805029519055aa62adacde339 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jul 2018 17:07:49 +0200
Subject: evarconv/evarsolve: HO matching algorithm with occurrence selection

Also extend evarconv to handle frozen evars and flags for delta and
betaiota reduction.

- Make evar_conv unification take a record of flags
- Adds an imitate_defs option to evarsolve, deactivated in first-order unification
- Add a way to call back  conv_algo differently on types

- We distinguish comparison of terms and types which might be different
w.r.t. delta reductions allowed (everything for types, controlled for
terms). We keep the with_cs flag even for types, to avoid
incompatibilities (in HoTT's theories/Spaces/No.v, the refine in
No_encode_le_lt would diverge due to trying a default canonical
structure during type verification).

- In evarsolve, do_project_effects checks evar instances now
- Solve evar-evar unification using miller patterns if possible.
- FO heuristic in evarconv
- Do not catch critical exceptions in evarconv
- Force HO matching to abstract toplevel evar args,
  This disallows K on them, more compatible with w_unify_to_subterm.
- occur_rigidly improvement, better approx of occur-check.

- K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into
  account in apply_on_subterm and evar_conv_x.
  This allow implementing a unification without reduction, e.g. for the
  fast path of rewrite subterm selection.
- second_order_matching works up-to cumulativity

- pretyping/coercion: now take unification flags as argument
- pretyping/unification: default_occurrence_test takes a frozen_evars set
  export elim_flags_evars to compute frozen evars before elim

- evarsolve: fix evar_define doing check in the wrong order,
  as conv_algo can trigger the definition of the evar itself,
  define it first in the evd.
- w_unify: disallow HO in consider_remaining. Only used in rewrite now
- use evar_abstraction info

- catch second_order_matching NoOccurrence exception in second_order_matching_with_args

- unify_with_heuristics in API

- second_order_matching: thin evars after abstraction to put in the
  right env or fail.
---
 engine/evd.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/evd.mli b/engine/evd.mli
index 1c852971f5..1f6a0da882 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -104,7 +104,7 @@ type evar_info = {
       in the solution *)
   evar_abstract_arguments : Abstraction.t;
   (** Boolean information over {!evar_hyps}, telling if an hypothesis instance
-      can be immitated or should stay abstract in HO unification problems
+      can be imitated or should stay abstract in HO unification problems
       and inversion (see [second_order_matching_with_args] for its use). *)
   evar_source : Evar_kinds.t located;
   (** Information about the evar. *)
-- 
cgit v1.2.3