diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 6821fc980..39f7de942 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -71,6 +71,8 @@ let eq_gname gn1 gn2 = String.equal s1 s2 && eq_constructor c1 c2 | Gconstant (s1, c1), Gconstant (s2, c2) -> String.equal s1 s2 && Constant.equal c1 c2 + | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) -> + String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2 | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2 | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2 | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2 @@ -86,7 +88,9 @@ let eq_gname gn1 gn2 = | Ginternal s1, Ginternal s2 -> String.equal s1 s2 | Grel i1, Grel i2 -> Int.equal i1 i2 | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 - | _ -> false + | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _ + | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ -> + false let dummy_gname = Grel 0 @@ -1645,15 +1649,15 @@ let pp_mllam fmt l = and pp_letrec fmt defs = let len = Array.length defs in - let pp_one_rec i (fn, argsn, body) = + let pp_one_rec (fn, argsn, body) = Format.fprintf fmt "%a%a =@\n %a" pp_lname fn pp_ldecls argsn pp_mllam body in Format.fprintf fmt "@[let rec "; - pp_one_rec 0 defs.(0); + pp_one_rec defs.(0); for i = 1 to len - 1 do Format.fprintf fmt "@\nand "; - pp_one_rec i defs.(i) + pp_one_rec defs.(i) done; and pp_blam fmt l = @@ -1841,7 +1845,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = in let auxdefs = List.fold_right get_rel_val fv_rel auxdefs in let auxdefs = List.fold_right get_named_val fv_named auxdefs in - let lvl = Context.Rel.length env.env_rel_context.env_rel_ctx in + let lvl = Context.Rel.length (rel_context env) in let fv_rel = List.map (fun (n,_) -> MLglobal (Grel (lvl-n))) fv_rel in let fv_named = List.map (fun (id,_) -> MLglobal (Gnamed id)) fv_named in let aux_name = fresh_lname Anonymous in @@ -1850,7 +1854,7 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = and compile_rel env sigma univ auxdefs n = let open Context.Rel.Declaration in let decl = lookup_rel n env in - let n = List.length env.env_rel_context.env_rel_ctx - n in + let n = List.length (rel_context env) - n in match decl with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in @@ -1937,7 +1941,7 @@ let is_code_loaded ~interactive name = let param_name = Name (Id.of_string "params") let arg_name = Name (Id.of_string "arg") -let compile_mind prefix ~interactive mb mind stack = +let compile_mind mb mind stack = let u = Declareops.inductive_polymorphic_context mb in (** Generate data for every block *) let f i stack ob = @@ -2016,7 +2020,7 @@ let compile_mind_deps env prefix ~interactive then init else let comp_stack = - compile_mind prefix ~interactive mib mind comp_stack + compile_mind mib mind comp_stack in let name = if interactive then LinkedInteractive prefix @@ -2088,9 +2092,9 @@ let compile_constant_field env prefix con acc cb = in gl@acc -let compile_mind_field prefix mp l acc mb = +let compile_mind_field mp l acc mb = let mind = MutInd.make2 mp l in - compile_mind prefix ~interactive:false mb mind acc + compile_mind mb mind acc let mk_open s = Gopen s |