diff options
author | 2015-02-23 19:48:54 +0100 | |
---|---|---|
committer | 2015-02-23 20:19:20 +0100 | |
commit | d64b5766aa8de3842edae167ce554c36ff46f947 (patch) | |
tree | f2b5a8f4c52d6af8a686d14db4500de13bb264b7 | |
parent | 152d8a93bbb70ca6ad6a7cd629bd508fd16c1a44 (diff) |
Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable_in.
-rw-r--r-- | pretyping/evarsolve.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index b01f29a40..307edcc89 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1017,7 +1017,7 @@ exception CannotProject of evar_map * existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t = +let rec is_constrainable_in top force env evd k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect t in match kind_of_term f with | Construct ((ind,_),u) -> @@ -1025,21 +1025,21 @@ let rec is_constrainable_in top force k (ev,(fv_rels,fv_ids) as g) t = if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false force k g) params - | Ind _ -> Array.for_all (is_constrainable_in false force k g) args - | Prod (_,t1,t2) -> is_constrainable_in false force k g t1 && is_constrainable_in false force k g t2 + Array.for_all (is_constrainable_in false force env evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false force env evd k g) args + | Prod (_,t1,t2) -> is_constrainable_in false force env evd k g t1 && is_constrainable_in false force env evd k g t2 | Evar (ev',_) -> top || not (force || Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels | Sort _ -> true - | _ -> (* We don't try to be more clever *) true + | _ -> (* We don't try to be more clever *) not force || noccur_evar env evd ev t -let has_constrainable_free_vars evd aliases force k ev (fv_rels,fv_ids as fvs) t = +let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids as fvs) t = let t = expansion_of_var aliases t in match kind_of_term t with | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels - | _ -> is_constrainable_in true force k (ev,fvs) t + | _ -> is_constrainable_in true force env evd k (ev,fvs) t exception EvarSolvedOnTheFly of evar_map * constr @@ -1049,7 +1049,7 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 - (has_constrainable_free_vars evd aliases force k2 evk2 fvs2) + (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2) argsv1 in let candidates1 = try restrict_candidates g env evd filter1 ev1 ev2 |