From 0d03f17a33b43aa87bb201953e4e1a567aac6355 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 31 Dec 2008 10:57:09 +0000
Subject: Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod
 -> splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added
 shortcuts for "fst (decompose_prod t)" and co.

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

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 99f439224c..e8860c065c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -163,7 +163,7 @@ let cs_pattern_of_constr t =
 let compute_canonical_projections (con,ind) =
   let v = mkConst con in
   let c = Environ.constant_value (Global.env()) con in
-  let lt,t = Reductionops.splay_lambda (Global.env()) Evd.empty c in
+  let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in
   let lt = List.rev (List.map snd lt) in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = 
@@ -234,7 +234,7 @@ 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 body = snd (splay_lambda (Global.env()) Evd.empty vc) in
+  let body = snd (splay_lam (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
-- 
cgit v1.2.3