diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 15:38:39 +0100 |
| commit | d016f69818b30b75d186fb14f440b93b0518fc66 (patch) | |
| tree | 32cd948273f79a2c01ad27b4ed0244ea60d7e2f9 /engine/evd.mli | |
| parent | b680b06b31c27751a7d551d95839aea38f7fbea1 (diff) | |
[coq] Untabify the whole ML codebase.
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 5ab53947f7..7876e9a48f 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -141,7 +141,7 @@ val empty : evar_map (** The empty evar map. *) val from_env : env -> evar_map -(** The empty evar map with given universe context, taking its initial +(** The empty evar map with given universe context, taking its initial universes from env. *) val from_ctx : UState.t -> evar_map @@ -251,7 +251,7 @@ val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr -val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> +val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map (** spiwack: this function seems to somewhat break the abstraction. *) @@ -596,8 +596,8 @@ val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_ val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map (** See [UState.make_nonalgebraic_variable]. *) -val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option -(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is +val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option +(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) val is_flexible_level : evar_map -> Univ.Level.t -> bool @@ -610,7 +610,7 @@ val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map -val set_eq_instances : ?flex:bool -> +val set_eq_instances : ?flex:bool -> evar_map -> Univ.Instance.t -> Univ.Instance.t -> evar_map val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool |