diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-21 17:05:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-21 17:06:49 +0100 |
| commit | dd888dffd48fbf74a83b9f3c07bbdeb63dc020a2 (patch) | |
| tree | 52448f53b692d3bbff4d87a09f15adac87211afe /pretyping/evd.ml | |
| parent | cf6a68b45b506be1dc2d37b0daefeaf18ff7c77a (diff) | |
Continuing experimentation on what part of the instance of an evar
to display by default (see bc8a5357889 - 17 Oct 2014):
- not printing instances for let-in anymore even when expanded (since
they are canonical up to conversion)
- still printing x:=x in [x:=x;x':=x] when x is directly an instance
of another var, but not in [x:=x;x':=S x]
This can be discussed, but if ever this is to be changed, it should
not be printed in [x:=x;x:=?n] with ?n implicitly depending on x
(otherwise said, variables which are not displayed in instances of
internal evars should not contribute to the decision of writing
x:=x in the instance).
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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 |