From 26a79004e47bbdc97df61015ce7e944eef14ac71 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Sep 2014 10:23:12 +0200
Subject: Parsing of Type@{max(i,j)}.

---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 plugins/funind/invfun.ml                | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 2ef3c34ed7..587af35acb 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1229,7 +1229,7 @@ let rec rebuild_return_type rt =
 	Constrexpr.CLetIn(loc,na,t,rebuild_return_type t')
     | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous],
 				       Constrexpr.Default Decl_kinds.Explicit,rt],
-			    Constrexpr.CSort(Loc.ghost,GType None))
+			    Constrexpr.CSort(Loc.ghost,GType []))
 
 
 let do_build_inductive
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 97157facd0..832e933a71 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1064,7 +1064,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	       (fun entry ->
 		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (Array.map_to_list (fun const -> const,GType None) funs))
+	       (make_scheme (Array.map_to_list (fun const -> const,GType []) funs))
 	    )
     in
     let proving_tac =
-- 
cgit v1.2.3