diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-11-22 17:12:58 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-06-14 07:19:50 +0200 |
| commit | daf5335b18c926d7130cd28e50f00cc49c4011f6 (patch) | |
| tree | f45377ea4597a3ba7699fa2e8b77046c7adc9b75 /pretyping | |
| parent | 571c319ed536cb2757176d3ae4007a75f5d3b04d (diff) | |
Remove support for Coq 8.3.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3e0eb9d91..ef4f7f754 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -484,8 +484,7 @@ let use_evars_pattern_unification flags = let use_metas_pattern_unification sigma flags nb l = !global_pattern_unification_flag && flags.use_pattern_unification - || (Flags.version_less_or_equal Flags.V8_3 || - flags.use_meta_bound_pattern_unification) && + || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l type key = @@ -608,9 +607,6 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) -let use_full_betaiota flags = - flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 - let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars) | _ -> false @@ -948,7 +944,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e expand curenvnb pb opt substn cM f1 l1 cN f2 l2 and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = - if use_full_betaiota flags && not (subterm_restriction opt flags) then + if flags.modulo_betaiota && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (EConstr.eq_constr sigma cM cM') then unirec_rec curenvnb pb opt substn cM' cN |