diff options
author | Matej Košík <matej.kosik@inria.fr> | 2017-06-07 14:25:07 +0200 |
---|---|---|
committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-07 14:49:13 +0200 |
commit | 34dd34065111c5abe68e88a79a77e482e79489a7 (patch) | |
tree | 624eb098d442a5b30e55729404830b8fe7bac0bb /plugins/ssr | |
parent | 661940fd55a925a6f17f6025f5d15fc9f5647cf9 (diff) |
Put "ssreflect" behind "API".
Diffstat (limited to 'plugins/ssr')
-rw-r--r-- | plugins/ssr/ssrast.mli | 3 | ||||
-rw-r--r-- | plugins/ssr/ssrbwd.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrbwd.mli | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 8 | ||||
-rw-r--r-- | plugins/ssr/ssrcommon.mli | 11 | ||||
-rw-r--r-- | plugins/ssr/ssrelim.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrelim.mli | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrequality.ml | 3 | ||||
-rw-r--r-- | plugins/ssr/ssrequality.mli | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrfwd.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrfwd.mli | 1 | ||||
-rw-r--r-- | plugins/ssr/ssripats.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssripats.mli | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.mli | 3 | ||||
-rw-r--r-- | plugins/ssr/ssrprinters.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrprinters.mli | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrtacticals.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrtacticals.mli | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrview.ml | 1 | ||||
-rw-r--r-- | plugins/ssr/ssrview.mli | 1 |
22 files changed, 39 insertions, 10 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 69202ae2d..4ddd38365 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Ltac_plugin @@ -78,7 +79,7 @@ type ssripat = | IPatView of ssrterm list (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl - | IPatNewHidden of identifier list + | IPatNewHidden of Id.t list (* | IPatVarsForAbstract of Id.t list *) and ssripats = ssripat list diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index cc0e86684..3988f00ba 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Printer open Pretyping open Globnames diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 8bf785a21..b0e98bdb4 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API + val apply_top_tac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma val inner_ssrapplytac : diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e90be92cf..38ee4be45 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Util open Names open Evd @@ -689,7 +691,7 @@ let pf_merge_uc_of sigma gl = let rec constr_name sigma c = match EConstr.kind sigma c with | Var id -> Name id | Cast (c', _, _) -> constr_name sigma c' - | Const (cn,_) -> Name (id_of_label (con_label cn)) + | Const (cn,_) -> Name (Label.to_id (con_label cn)) | App (c', _) -> constr_name sigma c' | _ -> Anonymous @@ -701,9 +703,9 @@ let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) (** look up a name in the ssreflect internals module *) -let ssrdirpath = make_dirpath [id_of_string "ssreflect"] +let ssrdirpath = DirPath.make [id_of_string "ssreflect"] let ssrqid name = Libnames.make_qualid ssrdirpath (id_of_string name) -let ssrtopqid name = Libnames.make_short_qualid (id_of_string name) +let ssrtopqid name = Libnames.qualid_of_ident (id_of_string name) let locate_reference qid = Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 834b7b722..1b6a700b2 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Environ open Proof_type @@ -173,12 +174,12 @@ val pf_type_id : Proof_type.goal Evd.sigma -> EConstr.types -> Id.t val pf_abs_evars : Proof_type.goal Evd.sigma -> evar_map * EConstr.t -> - int * EConstr.t * Constr.existential_key list * + int * EConstr.t * Evar.t list * Evd.evar_universe_context val pf_abs_evars2 : (* ssr2 *) Proof_type.goal Evd.sigma -> Evar.t list -> evar_map * EConstr.t -> - int * EConstr.t * Constr.existential_key list * + int * EConstr.t * Evar.t list * Evd.evar_universe_context val pf_abs_cterm : Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t @@ -214,7 +215,7 @@ val pf_mkSsrConst : string -> Proof_type.goal Evd.sigma -> EConstr.t * Proof_type.goal Evd.sigma -val new_wild_id : tac_ctx -> Names.identifier * tac_ctx +val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : @@ -228,7 +229,7 @@ val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : - tac_ctx -> (Names.identifier * Names.name ref) * tac_ctx + tac_ctx -> (Names.Id.t * Names.name ref) * tac_ctx val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Proof_type.goal Evd.sigma -> @@ -252,7 +253,7 @@ val red_product_skip_id : env -> evar_map -> EConstr.t -> EConstr.t val ssrautoprop_tac : - (Constr.existential_key Evd.sigma -> Constr.existential_key list Evd.sigma) ref + (Evar.t Evd.sigma -> Evar.t list Evd.sigma) ref val mkProt : EConstr.t -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 832044909..bd9a05891 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Util open Names open Printer diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index fb1b58ac3..8dc28d8b7 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin val ssrelim : diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index af315aac5..dbe13aec9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ltac_plugin open Util open Names @@ -343,7 +344,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = Term.destConst elim in let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in - let l' = label_of_id (Nameops.add_suffix (id_of_label l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 9c5fd4983..f712002c1 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin open Ssrast diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 663bca15e..2b10f2f35 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Tacmach diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 6fb97d524..ead361745 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index b850b0e95..96a75ba27 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Pp open Term diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index e90e75552..5f5c7f34a 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin open Ssrast open Ssrcommon diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 1fba39150..5fd377233 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index bf6f44f11..154820666 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,6 +8,9 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API + val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706..427109c1b 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Pp open Names open Printer diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 56ec145ad..9207b9e43 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrast val pp_term : diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 0fe8fdc26..67b705190 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Constr open Termops diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index b8e95b2b1..1d1887138 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API + val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> Ltac_plugin.Tacinterp.Value.t -> diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index b154cf217..6fbfbf03c 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Names open Term open Termops diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 3c995b1bb..91e40f368 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Util open Names open Term diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index 6fd906ff4..8a7bd5d6e 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrast open Ssrcommon |