diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 36 |
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 |