diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-10 11:39:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | c2855a3387be134d1220f301574b743572a94239 (patch) | |
| tree | 441b773053d953ccc38f555c1f45e524411663d9 /engine/termops.mli | |
| parent | 85ab3e298aa1d7333787c1fa44d25df189ac255c (diff) | |
Unification API using EConstr.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 2b66c88a7..df3fdd124 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -29,7 +29,7 @@ val print_rel_context : env -> std_ppcmds val print_env : env -> std_ppcmds (** about contexts *) -val push_rel_assum : Name.t * types -> env -> env +val push_rel_assum : Name.t * EConstr.types -> env -> env val push_rels_assum : (Name.t * types) list -> env -> env val push_named_rec_types : Name.t array * types array * 'a -> env -> env @@ -208,8 +208,8 @@ val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array val adjust_app_list_size : constr -> constr list -> constr -> constr list -> (constr * constr list * constr * constr list) -val adjust_app_array_size : constr -> constr array -> constr -> constr array -> - (constr * constr array * constr * constr array) +val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> + (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array) (** name contexts *) type names_context = Name.t list |