From 70c88a5f6d7e1ef184d70512969a6221eec8d11e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 9 Dec 2006 14:56:43 +0000
Subject: Évitement noms de constructeurs dans les motifs de filtrage de
 "match" (suite)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9425 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/impargs.ml b/library/impargs.ml
index b5488031bf..1dcbcead88 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -170,7 +170,7 @@ let add_free_rels_until strict bound env m pos acc =
 let my_concrete_name avoid names t = function
   | Anonymous -> Anonymous, avoid, Anonymous::names
   | na -> 
-      let id = Termops.next_name_not_occuring false na avoid names t in
+      let id = Termops.next_name_not_occuring None na avoid names t in
       Name id, id::avoid, Name id::names
   
 let compute_implicits_gen strict contextual env t =
@@ -178,7 +178,7 @@ let compute_implicits_gen strict contextual env t =
     let t = whd_betadeltaiota env t in
     match kind_of_term t with
       | Prod (na,a,b) ->
-	  let na',avoid' = Termops.concrete_name false avoid names na b in
+	  let na',avoid' = Termops.concrete_name None avoid names na b in
 	  add_free_rels_until strict n env a (Hyp (n+1))
             (aux (push_rel (na',None,a) env) avoid' (n+1) (na'::names) b)
       | _ -> 
@@ -189,7 +189,7 @@ let compute_implicits_gen strict contextual env t =
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
     | Prod (na,a,b) ->
-	let na',avoid = Termops.concrete_name false [] [] na b in
+	let na',avoid = Termops.concrete_name None [] [] na b in
 	let v = aux (push_rel (na',None,a) env) avoid 1 [na'] b in
 	Array.to_list v
     | _ -> []
-- 
cgit v1.2.3