diff options
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 23 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
3 files changed, 23 insertions, 5 deletions
diff --git a/dev/include b/dev/include index f785573ceb..9518034df1 100644 --- a/dev/include +++ b/dev/include @@ -44,6 +44,7 @@ (*#install_printer (* proof *) pproof;;*) #install_printer (* Goal.goal *) ppgoalgoal;; #install_printer (* metaset.t *) ppmetas;; +#install_printer (* evar *) ppevar;; #install_printer (* evar_map *) ppevm;; #install_printer (* Evar.Set.t *) ppexistentialset;; #install_printer (* clenv *) ppclenv;; diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 288ec6214f..20a4a3f9e3 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -305,7 +305,7 @@ let remove_instance_local_defs evd evk args = let rec aux sign i = match sign with | [] -> let () = assert (i = len) in [] - | (_, None _, _) :: sign -> + | (_, None, _) :: sign -> let () = assert (i < len) in (Array.unsafe_get args i) :: aux sign (succ i) | (_, Some _, _) :: sign -> @@ -1248,8 +1248,25 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = imitate envk t in let rhs = whd_beta evd rhs (* heuristic *) in - let body = imitate (env,0) rhs in - (!evdref,body) + let fast rhs = + let filter_ctxt = evar_filtered_context evi in + let names = ref Idset.empty in + let rec is_id_subst ctxt s = + match ctxt, s with + | ((id, _, _) :: ctxt'), (c :: s') -> + names := Idset.add id !names; + isVarId id c && is_id_subst ctxt' s' + | [], [] -> true + | _ -> false + in + is_id_subst filter_ctxt (Array.to_list argsv) && + closed0 rhs && + Idset.subset (collect_vars rhs) !names + in + let body = + if fast rhs then nf_evar evd rhs + else imitate (env,0) rhs + in (!evdref,body) (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b9b076d4fd..9c3b5c4dff 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -503,9 +503,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag with ex when precatchable_exception ex -> try reduce curenvnb pb b false substn cM cN with ex when precatchable_exception ex -> - try expand curenvnb pb b false substn cM f1 l1 cN f2 l2 + try canonical_projections curenvnb pb b cM cN substn with ex when precatchable_exception ex -> - canonical_projections curenvnb pb b cM cN substn + expand curenvnb pb b false substn cM f1 l1 cN f2 l2 and unify_not_same_head curenvnb pb b wt substn cM cN = try canonical_projections curenvnb pb b cM cN substn |