Removing useless filter allocation in evar construction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16940 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 19 insertions, 18 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b9a8743330..288ec6214f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -889,7 +889,7 @@ let are_canonical_instances args1 args2 env =
   Int.equal n1 n2 && aux 0 (named_context env)
 
 let filter_compatible_candidates conv_algo env evd evi args rhs c =
-  let c' = instantiate_evar_array (evar_filtered_context evi) c args in
+  let c' = instantiate_evar_array evi c args in
   match conv_algo env evd Reduction.CONV rhs c' with
   | Success evd -> Some (c,evd)
   | UnifFailure _ -> None
@@ -906,7 +906,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
   | None, Some _ -> raise DoesNotPreserveCandidateRestriction
   | Some l1, Some l2 ->
       let l1' = List.filter (fun c1 ->
-        let c1' = instantiate_evar_array (evar_filtered_context evi1) c1 argsv1 in
+        let c1' = instantiate_evar_array evi1 c1 argsv1 in
         let filter c2 =
           let compatibility = filter_compatible_candidates conv_algo env evd evi2 argsv2 c1' c2 in
           match compatibility with
@@ -1147,8 +1147,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
           let ty = find_solution_type (evar_filtered_env evi) sols in
-          let sign = evar_filtered_context evi in
-          let ty' = instantiate_evar_array sign ty argsv in
+          let ty' = instantiate_evar_array evi ty argsv in
           let (evd,evar,(evk',argsv' as ev')) =
             materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
           let ts = expansions_of_var aliases t in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e1bee21500..189408a981 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -187,20 +187,24 @@ let make_evar_instance sign args =
   in
   instrec sign args
 
-let make_evar_instance_array sign args =
+let make_evar_instance_array info args =
   let len = Array.length args in
-  let rec instrec sign i = match sign with
-  | [] ->
+  let rec instrec filter ctxt i = match filter, ctxt with
+  | [], [] ->
     if Int.equal i len then []
     else instance_mismatch ()
-  | (id, _, _) :: sign ->
+  | false :: filter, _ :: ctxt ->
+    instrec filter ctxt i
+  | true :: filter, (id, _, _) :: ctxt ->
     if i < len then
       let c = Array.unsafe_get args i in
-      if isVarId id c then instrec sign (succ i)
-      else (id, c) :: instrec sign (succ i)
+      if isVarId id c then instrec filter ctxt (succ i)
+      else (id, c) :: instrec filter ctxt (succ i)
     else instance_mismatch ()
+  | _ -> instance_mismatch ()
   in
-  instrec sign 0
+  let filter = Filter.repr (evar_filter info) in
+  instrec filter (evar_context info) 0
 
 let instantiate_evar sign c args =
   let inst = make_evar_instance sign args in
@@ -208,8 +212,8 @@ let instantiate_evar sign c args =
   | [] -> c
   | _ -> replace_vars inst c
 
-let instantiate_evar_array sign c args =
-  let inst = make_evar_instance_array sign args in
+let instantiate_evar_array info c args =
+  let inst = make_evar_instance_array info args in
   match inst with
   | [] -> c
   | _ -> replace_vars inst c
@@ -397,10 +401,9 @@ let is_undefined d e = EvMap.mem e d.undf_evars
 
 let existential_value d (n, args) =
   let info = find d n in
-  let hyps = evar_filtered_context info in
   match evar_body info with
   | Evar_defined c ->
-    instantiate_evar_array hyps c args
+    instantiate_evar_array info c args
   | Evar_empty ->
     raise NotInstantiatedEvar
 
@@ -413,8 +416,7 @@ let existential_type d (n, args) =
     try find d n
     with Not_found ->
       anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in
-  let hyps = evar_filtered_context info in
-    instantiate_evar_array hyps info.evar_concl args
+  instantiate_evar_array info info.evar_concl args
 
 let add_constraints d cstrs =
   { d with univ_cstrs = Univ.merge_constraints cstrs d.univ_cstrs }
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e23400a07c..17e9dedafa 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -219,7 +219,7 @@ val existential_opt_value : evar_map -> existential -> constr option
     exception. *)
 
 val instantiate_evar : named_context -> constr -> constr list -> constr
-val instantiate_evar_array : named_context -> constr -> constr array -> constr
+val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 (** Assume empty universe constraints in [evar_map] and [conv_pbs] *)