aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-23 11:20:06 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-09-23 11:20:06 +0000
commit0975092c808d31b3cae8aa3f036f48faad748aca (patch)
treefc7c2e805b661565e1d10da89b2dc84278ca603e
parentdfb12693947513e39461c46a67608ca8850798ec (diff)
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
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--test-suite/success/CanonicalStructure.v7
2 files changed, 10 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fa3a61afc..8ca06e9a5 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
diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index 003810cc2..44d21b83b 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -5,3 +5,10 @@ Structure foo : Type := Foo {
}.
Canonical Structure unopt_nat := @Foo nat (fun _ => O).
+
+(* Granted wish #1187 *)
+
+Record Silly (X : Set) : Set := mkSilly { x : X }.
+Definition anotherMk := mkSilly.
+Definition struct := anotherMk nat 3.
+Canonical Structure struct.