diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-02-09 18:53:53 +0100 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | cca57bcd89770e76e1bcc21eb41756dca2c51425 (patch) | |
| tree | a154d851847e26a8a757eddffc5371cbed85c68c /plugins/ssrmatching/ssrmatching.mli | |
| parent | 1523276aedcde1c79aff899ec87f05f3a708d13b (diff) | |
Porting the ssrmatching plugin to the new EConstr API.
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.mli')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 74a603e51..fa0c2f5b1 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -194,7 +194,7 @@ val mk_tpattern_matcher : (* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns * the conclusion of [gl] where [occ] occurrences of [t] have been replaced * by [Rel 1] and the instance of [t] *) -val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr +val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * EConstr.t (* It may be handy to inject a simple term into the first form of cpattern *) val cpattern_of_term : char * glob_constr_and_expr -> cpattern @@ -216,8 +216,8 @@ val assert_done : 'a option ref -> 'a [consider_remaining_unif_problems] and [resolve_typeclasses]. In case of failure they raise [NoMatch] *) -val unify_HO : env -> evar_map -> constr -> constr -> evar_map -val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma +val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map +val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma (** Some more low level functions needed to implement the full SSR language on top of the former APIs *) |