diff options
| -rw-r--r-- | pretyping/evarutil.ml | 17 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 12 |
2 files changed, 28 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 28473962a8..79d4467d8e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -436,6 +436,20 @@ and clear_hyps_in_evi evdref evi ids = let need_restriction k args = not (array_for_all (closedn k) args) +let rec expand_var env x = match kind_of_term x with + | Rel n -> + begin try match pi2 (lookup_rel n env) with + | Some t when isRel t -> expand_var env (lift n t) + | _ -> x + with Not_found -> x + end + | Var id -> + begin match pi2 (lookup_named id env) with + | Some t when isVar t -> expand_var env t + | _ -> x + end + | _ -> x + (* [find_projectable_vars env sigma y subst] finds all vars of [subst] * that project on [y] up to variables aliasing. In case of solutions that * differ only up to aliasing, the binding that requires the less @@ -465,7 +479,8 @@ type evar_projection = let rec find_projectable_vars env sigma y subst = let is_projectable (id,(idc,y')) = - if is_conv env sigma y y' then (idc,(y'=y,(id,ProjectVar))) + if y = y' or expand_var env y = expand_var env y' + then (idc,(y'=y,(id,ProjectVar))) else if isEvar y' then let (evk,argsv as t) = destEvar y' in let evi = Evd.find sigma evk in diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index ad69ced19e..26e62ae622 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -74,3 +74,15 @@ eauto. Check (exist _ O (refl_equal 0) : {n:nat|n=0}). Check (exist _ O I : {n:nat|True}). + +(* An example (initially from Marseille/Fairisle) that involves an evar with + different solutions (Input, Output or bool) that may or may not be + considered distinct depending on which kind of conversion is used *) + +Section A. +Definition STATE := (nat * bool)%type. +Let Input := bool. +Let Output := bool. +Parameter Out : STATE -> Output. +Check fun (s : STATE) (reg : Input) => reg = Out s. +End A. |