diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/evd.ml | 16 | ||||
| -rw-r--r-- | pretyping/evd.mli | 6 |
3 files changed, 17 insertions, 13 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0613a35016..dc1784f40c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -452,11 +452,13 @@ let rec check_and_clear_in_constr evdref err ids c = with ClearDependencyError (rid,err) -> raise (ClearDependencyError (List.assoc rid rids,err)) in - let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in - let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in + if rids = [] then c else begin + let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in + let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in - mkEvar(evk', Array.of_list nargs) + mkEvar(evk', Array.of_list nargs) + end | _ -> map_constr (check_and_clear_in_constr evdref err ids) c diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1c47b8b00d..9035bb54db 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -91,6 +91,7 @@ module EvarInfoMap = struct let remove evc k = ExistentialMap.remove k evc let mem evc k = ExistentialMap.mem k evc let fold = ExistentialMap.fold + let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false let add evd evk newinfo = ExistentialMap.add evk newinfo evd @@ -312,9 +313,11 @@ module EvarMap = struct let existential_value (sigma,_) = EvarInfoMap.existential_value sigma let existential_type (sigma,_) = EvarInfoMap.existential_type sigma let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma - let eq_evar_map x y = x == y || - (EvarInfoMap.equal eq_evar_info (fst x) (fst y) && - UniverseMap.equal (=) (snd x) (snd y)) + let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) && + (EvarInfoMap.exists sigma1 + (fun k v -> v.evar_body = Evar_empty && + (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty) + || not (UniverseMap.equal (=) sm1 sm2)) let merge e e' = fold (fun n v sigma -> add sigma n v) e' e @@ -427,10 +430,9 @@ type evar_map = (*** Lifting primitive from EvarMap. ***) -(* spiwack: this function seems to be used only for the definition of the progress - tactical. I would recommand not using it in other places. *) -let eq_evar_map d1 d2 = - EvarMap.eq_evar_map d1.evars d2.evars +(* HH: The progress tactical now uses this function. *) +let progress_evar_map d1 d2 = + EvarMap.progress_evar_map d1.evars d2.evars (* spiwack: tentative. It might very well not be the semantics we want for merging evar_map *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index bffcf1cc64..fed11f1ffa 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -121,9 +121,9 @@ type evar_map (* Unification state and existential variables *) -(* spiwack: this function seems to be used only for the definition of the progress - tactical. I would recommand not using it in other places. *) -val eq_evar_map : evar_map -> evar_map -> bool +(* Assuming that the second map extends the first one, this says if + some existing evar has been refined *) +val progress_evar_map : evar_map -> evar_map -> bool val empty : evar_map val is_empty : evar_map -> bool |