From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
---
 vernac/auto_ind_decl.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/auto_ind_decl.ml')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f715459616..cc59a96834 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -351,13 +351,13 @@ let build_beq_scheme mode kn =
             done;
 
           ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a))
-                        (mkCase (ci,do_predicate rel_list nb_cstr_args,NoInvert,
-                                  mkVar (Id.of_string "Y") ,ar2))
+                        (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args,
+                                  NoInvert, mkVar (Id.of_string "Y") ,ar2))))
                          (constrsi.(i).cs_args))
         done;
         mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))
+            mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar))))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
-- 
cgit v1.2.3