From 0975092c808d31b3cae8aa3f036f48faad748aca Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 23 Sep 2006 11:20:06 +0000
Subject: Wish #1187 granted (support for canonical structures that are records
 only up to some preliminary reductions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9166 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fa3a61afce..8ca06e9a5f 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -20,6 +20,7 @@ open Libobject
 open Library
 open Classops
 open Mod_subst
+open Reductionops
 
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
@@ -197,7 +198,8 @@ let check_and_decompose_canonical_structure ref =
   let vc = match Environ.constant_opt_value env sp with
     | Some vc -> vc
     | None -> error_not_structure ref in
-  let f,args = match kind_of_term (snd (decompose_lam vc)) with
+  let body = snd (splay_lambda (Global.env()) Evd.empty vc) in
+  let f,args = match kind_of_term body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
   let indsp = match kind_of_term f with
-- 
cgit v1.2.3