diff options
| author | Matthieu Sozeau | 2014-07-20 22:29:44 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-20 22:46:28 +0200 |
| commit | fd62149f9bf40b3f309ebbfd7497ef7c185436d5 (patch) | |
| tree | 0cfbdb91d5c904b8e4dc13cf5cb8579c5e2ab227 /pretyping | |
| parent | 77df7b1283940d979d3e14893d151bc544f41410 (diff) | |
Use kernel conversion on terms that contain universe variables during unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 |
3 files changed, 4 insertions, 9 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3b82e52a3b..dfaff327ab 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -445,10 +445,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail ?(cumul=true) loc env evd rigidonly v t c1 = - try if cumul then - (the_conv_x_leq env t c1 evd, v) - else (the_conv_x env t c1 evd, v) +let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> @@ -468,7 +466,7 @@ let rec inh_conv_coerce_to_fail ?(cumul=true) loc env evd rigidonly v t c1 = | _ -> name in let env1 = push_rel (name,None,u1) env in let (evd', v1) = - inh_conv_coerce_to_fail ~cumul:false loc env1 evd rigidonly + inh_conv_coerce_to_fail loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d6e8a96606..b0718ed7ec 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -135,9 +135,6 @@ let has_undefined_evars or_sorts evd t = has_ev c; Array.iter has_ev args | Evar_empty -> raise NotInstantiatedEvar) - | Ind (_,l) | Const (_,l) | Construct (_,l) - when or_sorts && not (Univ.Instance.is_empty l) -> - raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ed3459a524..a003716f9b 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1589,7 +1589,7 @@ let pr_evar_universe_context ctx = (str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universe_context_set ctx.uctx_local) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++h 0 (Univ.LSet.pr ctx.uctx_univ_algebraic) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables)) + h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) let print_env_short env = let pr_body n = function |