Pretyping cleanup: remove constr_of_global calls

1 files changed, 6 insertions, 6 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a98..56f5d521a3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign =
 	   (Some ([], 0, 0, [])) eqnpats pats
 	 in match acc with
 	     None -> c
-	   | Some (sign, len, _, c') ->
-	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c'))
-		 (lift_rel_context liftsign sign)
-	       in
-		 conj :: c)
+	    | Some (sign, len, _, c') ->
+               let sigma, conj = mk_coq_and !evdref c' in
+               let sigma, neg = mk_coq_not sigma conj in
+	       let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in
+               evdref := sigma; conj :: c)
       [] prevpatterns
   in match diffs with [] -> None
-    | _ -> Some (mk_coq_and diffs)
+    | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj)
 
 let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
   let i = ref 0 in