diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 6 | ||||
| -rw-r--r-- | proofs/logic.ml | 17 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 4 | ||||
| -rw-r--r-- | proofs/refine.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 |
5 files changed, 17 insertions, 16 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d64cd9fff..f4ac094b8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -67,7 +67,7 @@ let refresh_undefined_univs clenv = let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t -let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) (EConstr.of_constr c) exception NotExtensibleClause @@ -667,8 +667,8 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = - let t = Retyping.get_type_of env sigma ev in - let ty = Retyping.get_type_of env sigma c in + let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in + let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in let (ev, _) = destEvar ev in diff --git a/proofs/logic.ml b/proofs/logic.ml index 0fa193065..2df626e1c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -319,18 +319,19 @@ let check_conv_leq_goal env sigma arg ty conclty = else raise (RefinerError (BadType (arg,ty,conclty))) else sigma -exception Stop of constr list +exception Stop of EConstr.t list let meta_free_prefix sigma a = try + let a = Array.map EConstr.of_constr a in let _ = Array.fold_left (fun acc a -> - if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) + if occur_meta sigma a then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc let goal_type_of env sigma c = if !check then unsafe_type_of env sigma c - else Retyping.get_type_of env sigma c + else Retyping.get_type_of env sigma (EConstr.of_constr c) let rec mk_refgoals sigma goal goalacc conclty trm = let env = Goal.V82.env sigma goal in @@ -339,7 +340,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then - let t'ty = Retyping.get_type_of env sigma trm in + let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) else @@ -372,7 +373,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (* Template sort-polymorphism of definition and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in - type_of_global_reference_knowing_parameters env sigma f args + type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) in goalacc, ty, sigma, f else @@ -386,7 +387,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | Case (ci,p,c,lf) -> @@ -435,7 +436,7 @@ and mk_hdgoals sigma goal goalacc trm = if is_template_polymorphic env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in - (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) + (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f) else mk_hdgoals sigma goal goalacc f in let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in @@ -460,7 +461,7 @@ and mk_hdgoals sigma goal goalacc trm = | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in let c = mkProj (p, c') in - let ty = get_type_of env sigma c in + let ty = get_type_of env sigma (EConstr.of_constr c) in (acc',ty,sigma,c) | _ -> diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 62fe2c17c..19e72e697 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -24,7 +24,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp) let warn_native_compute_disabled = @@ -37,7 +37,7 @@ let cbv_native env sigma c = (warn_native_compute_disabled (); cbv_vm env sigma c) else - let ctyp = Retyping.get_type_of env sigma (EConstr.Unsafe.to_constr c) in + let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp) let whd_cbn flags env sigma t = diff --git a/proofs/refine.ml b/proofs/refine.ml index d4920e505..e6e3ef47d 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,7 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in + let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 09f5246ab..b63b2ce28 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -104,7 +104,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls +let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -230,7 +230,7 @@ module New = struct let pf_hnf_constr gl t = pf_reduce hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (pf_get_type_of gl t) + pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t |