diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 2 | ||||
| -rw-r--r-- | engine/eConstr.mli | 2 | ||||
| -rw-r--r-- | engine/evarutil.ml | 7 | ||||
| -rw-r--r-- | engine/evarutil.mli | 8 | ||||
| -rw-r--r-- | engine/termops.ml | 1 | ||||
| -rw-r--r-- | engine/termops.mli | 8 |
6 files changed, 17 insertions, 11 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 0a5f1ba685..095521e252 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -75,6 +75,8 @@ type constr = t type existential = t pexistential type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint +type unsafe_judgment = (constr, types) Environ.punsafe_judgment +type unsafe_type_judgment = types Environ.punsafe_type_judgment let mkProp = of_kind (Sort Sorts.prop) let mkSet = of_kind (Sort Sorts.set) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 03e2d4ffcc..10eb064a3c 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -20,6 +20,8 @@ type constr = t type existential = t pexistential type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint +type unsafe_judgment = (constr, types) Environ.punsafe_judgment +type unsafe_type_judgment = types Environ.punsafe_type_judgment (** {5 Destructors} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index fc193b94a1..bc55ac4580 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -96,14 +96,15 @@ let rec whd_evar sigma c = | _ -> c let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t) +let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t)) let j_nf_evar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = nf_evar sigma j.uj_type } + { uj_val = e_nf_evar sigma j.uj_val; + uj_type = e_nf_evar sigma j.uj_type } let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl let jv_nf_evar sigma = Array.map (j_nf_evar sigma) let tj_nf_evar sigma {utj_val=v;utj_type=t} = - {utj_val=nf_evar sigma v;utj_type=t} + {utj_val=e_nf_evar sigma v;utj_type=t} let nf_evars_universes evm = Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index dcb9bf2472..8f3c3c352c 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -141,13 +141,13 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma val whd_evar : evar_map -> constr -> constr val nf_evar : evar_map -> constr -> constr -val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment +val j_nf_evar : evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment val jl_nf_evar : - evar_map -> unsafe_judgment list -> unsafe_judgment list + evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list val jv_nf_evar : - evar_map -> unsafe_judgment array -> unsafe_judgment array + evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array val tj_nf_evar : - evar_map -> unsafe_type_judgment -> unsafe_type_judgment + evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t diff --git a/engine/termops.ml b/engine/termops.ml index c1198e05aa..83f07d2c62 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1141,6 +1141,7 @@ let impossible_default_case = ref None let set_impossible_default_clause c = impossible_default_case := Some c let coq_unit_judge = + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in let na1 = Name (Id.of_string "A") in let na2 = Name (Id.of_string "H") in fun () -> diff --git a/engine/termops.mli b/engine/termops.mli index df3fdd124e..27b3ea53ca 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -274,10 +274,10 @@ val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool (** Combinators on judgments *) -val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment +val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment +val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment (** {6 Functions to deal with impossible cases } *) val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set |