diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 03:04:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:31 +0100 |
| commit | d833b81b49366e95cf20a1d00f9c63883adb8942 (patch) | |
| tree | 1afca49fcd42e96b658c90d28e9da692ccc39724 /engine | |
| parent | c0d38ae52ac410811e7df54c52e8d3a18bb11bcb (diff) | |
Rewrite API using EConstr.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 3 | ||||
| -rw-r--r-- | engine/evarutil.mli | 4 | ||||
| -rw-r--r-- | engine/termops.ml | 5 | ||||
| -rw-r--r-- | engine/termops.mli | 2 |
4 files changed, 11 insertions, 3 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 8b75d8242..204997445 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -463,12 +463,13 @@ let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = c let new_Type ?(rigid=Evd.univ_flexible) env evd = + let open EConstr in let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in Sigma (mkSort s, sigma, p) let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = let evd', s = new_sort_variable rigid !evdref in - evdref := evd'; mkSort s + evdref := evd'; EConstr.mkSort s (* The same using side-effect *) let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 1b592b790..cf36f5953 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -52,8 +52,8 @@ val e_new_type_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> EConstr.constr * sorts -val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (EConstr.constr, 'r) Sigma.sigma +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> EConstr.constr val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> constr list option -> (existential_key, 'r) Sigma.sigma diff --git a/engine/termops.ml b/engine/termops.ml index 7c89f190f..ecc6ab68e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -858,6 +858,11 @@ let base_sort_cmp pb s0 s1 = | (Type u1, Type u2) -> true | _ -> false +let rec is_Prop sigma c = match EConstr.kind sigma c with + | Sort (Prop Null) -> true + | Cast (c,_,_) -> is_Prop sigma c + | _ -> false + (* eq_constr extended with universe erasure *) let compare_constr_univ sigma f cv_pb t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with diff --git a/engine/termops.mli b/engine/termops.mli index a865c80fb..05604beda 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -275,6 +275,8 @@ val isGlobalRef : Evd.evar_map -> EConstr.t -> bool val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool +val is_Prop : Evd.evar_map -> EConstr.t -> bool + (** Combinators on judgments *) val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment |