Move to a representation of universe polymorphic constants using indices for variables.

Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.

1 files changed, 18 insertions, 18 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e6844673c..1f3e7b571 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -61,7 +61,7 @@ module ReductionBehaviour = struct
   let discharge = function
     | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
        let c' = pop_con c in
-       let vars, _ctx = Lib.section_segment_of_constant c in
+       let vars, _subst, _ctx = Lib.section_segment_of_constant c in
        let extra = List.length vars in
        let nargs' = if b.b_nargs < 0 then b.b_nargs else b.b_nargs + extra in
        let recargs' = List.map ((+) extra) b.b_recargs in
@@ -654,23 +654,23 @@ let reducible_mind_case c = match kind_of_term c with
 *)
 let magicaly_constant_of_fixbody env bd = function
   | Name.Anonymous -> bd
-  | Name.Name id ->
-    try
-      let cst = Nametab.locate_constant
-	(Libnames.make_qualid DirPath.empty id) in
-      let (cst, u), ctx = Universes.fresh_constant_instance env cst in
-      match constant_opt_value env (cst,u) with
-      | None -> bd
-      | Some (t,cstrs) -> 
-        let b, csts = Universes.eq_constr_universes t bd in
-	let subst = Universes.Constraints.fold (fun (l,d,r) acc -> 
-	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc)
-	  csts Univ.LMap.empty
-	in
-	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in
-          if b then mkConstU (cst,inst) else bd
-    with
-    | Not_found -> bd
+  | Name.Name id -> bd
+    (* try *)
+    (*   let cst = Nametab.locate_constant *)
+    (* 	(Libnames.make_qualid DirPath.empty id) in *)
+    (*   let (cst, u), ctx = Universes.fresh_constant_instance env cst in *)
+    (*   match constant_opt_value_in env (cst,u) with *)
+    (*   | None -> bd *)
+    (*   | Some t ->  *)
+    (*     let b, csts = Universes.eq_constr_universes t bd in *)
+    (* 	let subst = Universes.Constraints.fold (fun (l,d,r) acc ->  *)
+    (* 	  Univ.LMap.add (Option.get (Universe.level l)) (Option.get (Universe.level r)) acc) *)
+    (* 	  csts Univ.LMap.empty *)
+    (* 	in *)
+    (* 	let inst = Instance.subst_fn (fun u -> Univ.LMap.find u subst) u in *)
+    (*       if b then mkConstU (cst,inst) else bd *)
+    (* with *)
+    (* | Not_found -> bd *)
 
 let contract_cofix ?env (bodynum,(names,types,bodies as typedbodies)) =
   let nbodies = Array.length bodies in