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
---
 contrib/cc/cctac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/cc')

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index dcd0ea469c..515d4aa932 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -228,10 +228,10 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let ci=pred (snd cstr) in
   let branch i=
     let ti=Term.prod_appvect types.(i) argv in
-    let rc=fst (Sign.decompose_prod_assum ti) in
+    let rc=fst (decompose_prod_assum ti) in
     let head=
       if i=ci then special else default in  
-      Sign.it_mkLambda_or_LetIn head rc in
+      it_mkLambda_or_LetIn head rc in
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
   let pred=mkLambda(Anonymous,intype,outtype) in
-- 
cgit v1.2.3