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
---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index de2a0dacf0..d21d3e767b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -251,7 +251,7 @@ let find_elim hdcncl lft2rgt dep cls args gl =
 	  let c1 = destConst pr1 in 
 	  let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in 
 	  let l' = label_of_id (add_suffix (id_of_label l) "_r")  in 
-	  let c1' = Global.constant_of_delta (make_con mp dp l') in
+	  let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
-- 
cgit v1.2.3