From e79b800bec660dc2724fa70c33f4e435ddbf885c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 11 Oct 2011 09:06:05 +0000
Subject: Various simplifications about constant_of_delta and mind_of_delta

 Most of the time, a constant name is built from:
  - a kernel_name for its user part
  - a delta_resolver applied to this kernel_name for its canonical part
 With this patch we avoid building unnecessary constants for immediately
 amending them (cf in particular the awkward code removed in safe_typing).

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

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e1da61908a..b875912fcc 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -559,8 +559,7 @@ let lookup_eliminator ind_sp s =
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta
-      (make_con mp dp (label_of_id id)) in
+    let cst =Global.constant_of_delta_kn (make_kn mp dp (label_of_id id)) in
     let _ = Global.lookup_constant cst in
       mkConst cst
   with Not_found ->
-- 
cgit v1.2.3