From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 tactics/hints.ml   | 18 +++++++++---------
 tactics/tactics.ml |  5 +++--
 2 files changed, 12 insertions(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 748e0362c4..09b2e59cea 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -299,16 +299,16 @@ let strip_params env sigma c =
   match EConstr.kind sigma c with
   | App (f, args) -> 
     (match EConstr.kind sigma f with
-    | Const (p,_) ->
-      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)))
+    | Const (cst,_) ->
+      (match Recordops.find_primitive_projection cst with
+       | Some p ->
+         let p = Projection.make p false in
+         let npars = Projection.npars p in
+         if Array.length args > npars then
+           mkApp (mkProj (p, args.(npars)),
+                  Array.sub args (npars+1) (Array.length args - (npars + 1)))
          else c
-       | exception Not_found -> c)
+       | None -> c)
     | _ -> c)
   | _ -> c
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 928530744a..5fc34619e8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1581,9 +1581,10 @@ let make_projection env sigma params cstr sign elim i n c u =
       | Some proj ->
 	  let args = Context.Rel.to_extended_vect mkRel 0 sign in
 	  let proj =
-	    if Environ.is_projection proj env then
+            match Recordops.find_primitive_projection proj with
+            | Some proj ->
 	      mkProj (Projection.make proj false, mkApp (c, args))
-	    else
+            | None ->
 	      mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
 		[|mkApp (c, args)|])
 	  in
-- 
cgit v1.2.3