From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 checker/environ.ml | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

(limited to 'checker/environ.ml')

diff --git a/checker/environ.ml b/checker/environ.ml
index bbd043c8..b172acb1 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -164,14 +164,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let is_projection cst env = 
-  not (Option.is_empty (lookup_constant cst env).const_proj)
-
-let lookup_projection p env =
-  match (lookup_constant (Projection.constant p) env).const_proj with 
-  | Some pb -> pb
-  | None -> anomaly ("lookup_projection: constant is not a projection.")
-
 (* Mutual Inductives *)
 let scrape_mind env kn=
   try
@@ -191,7 +183,7 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    Printf.ksprintf anomaly ("Inductive %s is already defined.")
+    Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
@@ -201,10 +193,23 @@ let add_mind kn mib env =
     KNmap.add kn1 kn2  env.env_globals.env_inductives_eq in
   let new_globals =
     { env.env_globals with
-	env_inductives = new_inds;
-	env_inductives_eq = new_inds_eq} in
+      env_inductives = new_inds;
+      env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,labs,typs = infos.(i) in
+    let parg = Projection.arg p in
+    if not (Label.equal labs.(parg) (Projection.label p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection")
+    else if not (Int.equal mib.mind_nparams (Projection.npars p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection")
+    else typs.(parg)
 
 (* Modules *)
 
-- 
cgit v1.2.3