From 5de89439d459edd402328a1e437be4d8cd2e4f46 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Aug 2014 17:20:55 +0200
Subject: - Fix has_undefined_evars not using its or_sorts argument anymore. -
 Allow apply's unification to use conversion even if some polymorphic
 constants appear in the goal (consistent with occur_meta_or_evar, and
 evarconv in general).

---
 pretyping/evarutil.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/evarutil.ml')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b0718ed7ec..d14aa23a7e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -126,7 +126,7 @@ let nf_evar_map_undefined evm =
 (* Auxiliary functions for the conversion algorithms modulo evars
  *)
 
-let has_undefined_evars or_sorts evd t =
+let has_undefined_evars evd t =
   let rec has_ev t =
     match kind_of_term t with
     | Evar (ev,args) ->
@@ -140,7 +140,7 @@ let has_undefined_evars or_sorts evd t =
   with (Not_found | NotInstantiatedEvar) -> true
 
 let is_ground_term evd t =
-  not (has_undefined_evars true evd t)
+  not (has_undefined_evars evd t)
 
 let is_ground_env evd env =
   let is_ground_decl = function
-- 
cgit v1.2.3