diff options
| -rw-r--r-- | pretyping/evarsolve.ml | 28 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3755.v | 16 |
2 files changed, 25 insertions, 19 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 921609aae..adfe9dd8d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -64,30 +64,33 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) - and refresh_term_evars onevars t = + and refresh_term_evars onevars top t = match kind_of_term t with | App (f, args) when is_template_polymorphic env f -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos + | App (f, args) when top && isEvar f -> + refresh_term_evars true false f; + Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in let ty' = refresh true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () - | _ -> iter_constr (refresh_term_evars onevars) t + | _ -> iter_constr (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = let rec aux i = function | Some l :: ls -> if i < Array.length args then - ignore(refresh_term_evars true args.(i)); + ignore(refresh_term_evars true false args.(i)); aux (succ i) ls | None :: ls -> if i < Array.length args then - ignore(refresh_term_evars false args.(i)); + ignore(refresh_term_evars false false args.(i)); aux (succ i) ls | [] -> () in aux 0 pos @@ -97,7 +100,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = (match pbty with | None -> t | Some dir -> refresh dir t) - else (refresh_term_evars false t; t) + else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -1385,19 +1388,6 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - 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 rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in diff --git a/test-suite/bugs/closed/3755.v b/test-suite/bugs/closed/3755.v new file mode 100644 index 000000000..77427ace5 --- /dev/null +++ b/test-suite/bugs/closed/3755.v @@ -0,0 +1,16 @@ +(* File reduced by coq-bug-finder from original input, then from 6729 lines to +411 lines, then from 148 lines to 115 lines, then from 99 lines to 70 lines, +then from 85 lines to 63 lines, then from 76 lines to 55 lines, then from 61 +lines to 17 lines *) +(* coqc version trunk (January 2015) compiled on Jan 17 2015 21:58:5 with OCaml +4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk +(9e6b28c04ad98369a012faf3bd4d630cf123a473) *) +Set Printing Universes. +Section param. + Variable typeD : Set -> Set. + Variable STex : forall (T : Type) (p : T -> Set), Set. + Definition existsEach_cons' v (P : @sigT _ typeD -> Set) := + @STex _ (fun x => P (@existT _ _ v x)). + + Check @existT _ _ STex STex. |