From c7bd285555153294ec077cfa05c36bb420716f3b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 12 Apr 2018 21:41:03 +0200
Subject: Reduce circular dependency constants <-> projections

Instead of having the projection data in the constant data we have it
independently in the environment.
---
 tactics/hints.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7b5be4c1c..29744e406 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -293,15 +293,15 @@ let strip_params env sigma c =
   | App (f, args) -> 
     (match EConstr.kind sigma f with
     | Const (p,_) ->
-      let cb = lookup_constant p env in
-	(match cb.Declarations.const_proj with
-	| Some pb -> 
-	  let n = pb.Declarations.proj_npars in
-	    if Array.length args > n then
-	      mkApp (mkProj (Projection.make p false, args.(n)), 
-		     Array.sub args (n+1) (Array.length args - (n + 1)))
-	    else c
-	| None -> c)
+      let p = Projection.make p false in
+      (match lookup_projection p env with
+       | pb ->
+         let n = pb.Declarations.proj_npars in
+         if Array.length args > n then
+           mkApp (mkProj (p, args.(n)),
+                  Array.sub args (n+1) (Array.length args - (n + 1)))
+         else c
+       | exception Not_found -> c)
     | _ -> c)
   | _ -> c
 
-- 
cgit v1.2.3