diff options
| -rw-r--r-- | Makefile.build | 3 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1891.v | 13 |
3 files changed, 20 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build index ee9faca9f8..95f6b075cf 100644 --- a/Makefile.build +++ b/Makefile.build @@ -563,7 +563,8 @@ field: $(FIELDVO) $(FIELDCMO) fourier: $(FOURIERVO) $(FOURIERCMO) funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) -programs subtac: $(SUBTACVO) $(SUBTACCMO) +programs: $(PROGRAMSVO) +subtac: $(SUBTACVO) $(SUBTACCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) ########################################################################### diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index eb1035f2c8..3563c77887 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -567,16 +567,16 @@ type evar_projection = | ProjectVar | ProjectEvar of existential * evar_info * identifier * evar_projection -let rec find_projectable_vars env sigma y subst = +let rec find_projectable_vars with_evars env sigma y subst = let is_projectable (id,(idc,y')) = let y' = whd_evar sigma y' in if y = y' or expand_var env y = expand_var env y' then (idc,(y'=y,(id,ProjectVar))) - else if isEvar y' then + else if with_evars & isEvar y' then let (evk,argsv as t) = destEvar y' in let evi = Evd.find sigma evk in let subst = make_projectable_subst sigma evi argsv in - let l = find_projectable_vars env sigma y subst in + let l = find_projectable_vars with_evars env sigma y subst in match l with | [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p)))) | _ -> failwith "" @@ -595,7 +595,7 @@ let filter_solution = function | [id,p] -> (mkVar id, p) let project_with_effects env sigma effects t subst = - let c, p = filter_solution (find_projectable_vars env sigma t subst) in + let c, p = filter_solution (find_projectable_vars false env sigma t subst) in effects := p :: !effects; c @@ -849,7 +849,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = let project_variable t = (* Evar/Var problem: unifiable iff variable projectable from ev subst *) try - let sols = find_projectable_vars env (evars_of !evdref) t subst in + let sols = find_projectable_vars true env (evars_of !evdref) t subst in let c, p = filter_solution sols in let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in let evd = do_projection_effects evar_define env ty !evdref p in diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v new file mode 100644 index 0000000000..11124cddd7 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1891.v @@ -0,0 +1,13 @@ +(* Check evar-evar unification *) + Inductive T (A: Set): Set := mkT: unit -> T A. + + Definition f (A: Set) (l: T A): unit := tt. + + Implicit Arguments f [A]. + + Lemma L (x: T unit): (unit -> T unit) -> unit. + Proof. + refine (fun x => match x return _ with mkT n => fun g => f (g _) end). + trivial. + Qed. + |