diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/detyping.ml | 11 | ||||
-rw-r--r-- | pretyping/evd.ml | 10 | ||||
-rw-r--r-- | pretyping/evd.mli | 2 |
3 files changed, 12 insertions, 11 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 046ee0dad..28fb8cbe3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -498,16 +498,17 @@ let rec detype flags avoid env sigma t = else noparams () | Evar (evk,cl) -> - let bound_to_itself id c = + let bound_to_itself_or_letin (id,b,_) c = + b != None || try let n = List.index Name.equal (Name id) (fst env) in - isRelN n c + isRelN n c with Not_found -> isVarId id c in let id,l = try let id = Evd.evar_ident evk sigma in - let l = Evd.evar_instance_array bound_to_itself (Evd.find sigma evk) cl in - let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> (Id.Set.union fvs (collect_vars c), Int.Set.union rels (free_rels c))) (Id.Set.empty,Int.Set.empty) l in - let l = Evd.evar_instance_array (fun id c -> not !print_evar_arguments && (bound_to_itself id c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in + let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in + let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in + let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ee72d3147..9313e2232 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -230,20 +230,20 @@ let evar_instance_array test_id info args = else instance_mismatch () | false :: filter, _ :: ctxt -> instrec filter ctxt i - | true :: filter, (id, _, _) :: ctxt -> + | true :: filter, (id,_,_ as d) :: ctxt -> if i < len then let c = Array.unsafe_get args i in - if test_id id c then instrec filter ctxt (succ i) + if test_id d c then instrec filter ctxt (succ i) else (id, c) :: instrec filter ctxt (succ i) else instance_mismatch () | _ -> instance_mismatch () in match Filter.repr (evar_filter info) with | None -> - let map i (id, _, _) = + let map i (id,_,_ as d) = if (i < len) then let c = Array.unsafe_get args i in - if test_id id c then None else Some (id,c) + if test_id d c then None else Some (id,c) else instance_mismatch () in List.map_filter_i map (evar_context info) @@ -251,7 +251,7 @@ let evar_instance_array test_id info args = instrec filter (evar_context info) 0 let make_evar_instance_array info args = - evar_instance_array isVarId info args + evar_instance_array (fun (id,_,_) -> isVarId id) info args let instantiate_evar_array info c args = let inst = make_evar_instance_array info args in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b6c5d426f..cf6ba07c6 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -223,7 +223,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr |