From 509d958342764e4a676e735a3896f6ff77c07ff9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Feb 2020 11:38:15 +0100
Subject: New syntax [Inductive Acc A R | x : Prop := ...]

to control uniform parameters.

This replaces the attribute.
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fdbad2ab9e..c7dfe69fb1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1476,7 +1476,7 @@ let do_build_inductive
   in
   let rel_ind i ext_rel_constructors =
     ((CAst.make @@ relnames.(i)),
-    rel_params,
+    (rel_params,None),
     Some rel_arities.(i),
     ext_rel_constructors),[]
   in
-- 
cgit v1.2.3