From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sat, 29 Dec 2012 10:57:43 +0100
Subject: Imported Upstream version 8.4pl1dfsg

---
 plugins/funind/glob_term_to_relation.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c88c6669..43b08840 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -308,13 +308,14 @@ let build_constructors_of_type ind' argl =
 		    (Global.env ())
 		    construct
 		in
-		let argl =
-		  if argl = []
-		  then
+		let argl = match argl with
+                | None ->
  		    Array.to_list
-		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
+		      (Array.init cst_narg (fun _ -> mkGHole ())
 		      )
-		  else argl
+                | Some l ->
+	            Array.to_list
+		      (Array.init npar (fun _ -> mkGHole ()))@l
 		in
 		let pat_as_term =
 		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
@@ -653,7 +654,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
-	let case_pats = build_constructors_of_type ind [] in
+	let case_pats = build_constructors_of_type ind None in
 	assert (Array.length case_pats = 2);
 	let brl =
 	  list_map_i
@@ -669,12 +670,12 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GLetTuple(_,nal,_,b,e) ->
 	begin
 	  let nal_as_glob_constr =
-	    List.map
+	    Some (List.map
 	      (function
 		   Name id -> mkGVar id
 		 | Anonymous -> mkGHole ()
 	      )
-	      nal
+	      nal)
 	  in
 	  let b_as_constr = Pretyping.Default.understand Evd.empty env b in
 	  let b_typ = Typing.type_of env Evd.empty b_as_constr in
-- 
cgit v1.2.3