Add heuristic based on non-linearity of evars to determine whether an

evar is dependent or not (solve bug #2123).



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

1 files changed, 16 insertions, 0 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 9d2c56e6be..7e4c9358e5 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -116,11 +116,27 @@ let push_dependent_evars sigma emap =
       (sigma',emap') (collect_evars emap' ccl))
     emap (sigma,emap)
 
+let push_duplicated_evars sigma emap c = 
+  let rec collrec (one,(sigma,emap) as acc) c =
+    match kind_of_term c with
+    | Evar (evk,_) when not (Evd.mem sigma evk) ->
+	if List.mem evk one then
+	  let sigma' = Evd.add sigma evk (Evd.find emap evk) in
+	  let emap' = Evd.remove emap evk in
+	  (one,(sigma',emap'))
+	else
+	  (evk::one,(sigma,emap))
+    | _ ->
+	fold_constr collrec acc c
+  in
+  snd (collrec ([],(sigma,emap)) c)
+
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
 let evars_to_metas sigma (emap, c) =
   let emap = nf_evars emap in
   let sigma',emap' = push_dependent_evars sigma emap in
+  let sigma',emap' = push_duplicated_evars sigma' emap' c in
   let change_exist evar =
     let ty = nf_betaiota emap (existential_type emap evar) in
     let n = new_meta() in