diff options
| author | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
| commit | 915554785ffed11370f5d700d11a8b5614408096 (patch) | |
| tree | 4b5b4120c896cf99c863fab4fd5e1ec22af20d53 /plugins/ssr | |
| parent | ebe133a0df0656de82a566c4f1673257f60f7c0c (diff) | |
| parent | 9f47342d890dc3ef7f4950004513a47d940af5ca (diff) | |
Merge PR #6186: [api] Miscellaneous consolidation.
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 7 |
2 files changed, 3 insertions, 6 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 274c7110c6..bd9633afbd 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -342,7 +342,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let sort = elimination_sort_of_goal gl in let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) - let elim, _ = Term.destConst elim in + let elim, _ = destConst elim in let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index a707226cd0..5c1b399a80 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,11 +8,12 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open Pp open Names +open Constr open Tacmach open Ssrmatching_plugin.Ssrmatching - open Ssrprinters open Ssrcommon open Ssrtacticals @@ -30,10 +31,6 @@ let ssrposetac ist (id, (_, t)) gl = let sigma, t, ucst, _ = pf_abs_ssrterm ist gl t in posetac id t (pf_merge_uc ucst gl) -open Pp -open Term -open Constr - let ssrsettac ist id ((_, (pat, pty)), (_, occ)) gl = let pat = interp_cpattern ist gl pat (Option.map snd pty) in let cl, sigma, env = pf_concl gl, project gl, pf_env gl in |