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

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 00af99d980..c141a02aa3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -163,7 +163,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
 
-  begin  
+  begin
   match mind_of_delta reso2 kn2  with
       | kn2' when kn2=kn2' -> ()
       | kn2' -> 
-- 
cgit v1.2.3