From 3f5ce5cbf138435fcf7e50bf978192c9fdd7db05 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 9 Nov 2008 16:17:14 +0000
Subject: More factorization of inductive/record and typeclasses: move class
 declaration code to toplevel/record, including support for singleton classes
 as definitions. Parsing code also factorized. Arnaud: one more thing to think
 about when refactoring the definitions in vernacentries. Add support for
 specifying what to do with anonymous variables in contexts during
 internalisation (fixes bug #1982), current choice is to generate a name for
 typeclass bindings.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/funind/merge.ml               | 2 +-
 contrib/funind/rawterm_to_relation.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/funind')

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index b7cee73902..9bbd165dff 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
     List.map (* zeta_normalize t ? *)
       (fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
       rawlist in  
-  lident , bindlist , cstr_expr , lcstor_expr
+  lident , bindlist , Some cstr_expr , lcstor_expr
 
 
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index c16e645c73..75f6207fcc 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1192,7 +1192,7 @@ let do_build_inductive
   let rel_ind i ext_rel_constructors = 
     ((dummy_loc,relnames.(i)),
     rel_params,
-    rel_arities.(i),
+    Some rel_arities.(i),
     ext_rel_constructors),None
   in
   let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in 
-- 
cgit v1.2.3