Put "ssreflect" behind "API".

25 files changed, 67 insertions, 12 deletions

diff --git a/.gitignore b/.gitignore
index fe5f59b94..84fe89d1e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -180,3 +180,6 @@ test-suite/.nra.cache
 # these files are generated from plugins/micromega/MExtraction.v
 plugins/micromega/micromega.ml
 plugins/micromega/micromega.mli
+
+plugins/ssr/ssrparser.ml
+plugins/ssr/ssrvernac.ml
diff --git a/API/API.mli b/API/API.mli
index 2661badc5..d844e8bf5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -809,6 +809,7 @@ sig
   val mkNamedLambda : Names.Id.t -> types -> constr -> constr
   val mkNamedProd : Names.Id.t -> types -> types -> types
 
+  val isCast : Evd.evar_map -> t -> bool
   val isEvar : Prelude.evar_map -> constr -> bool
   val isInd  : Prelude.evar_map -> constr -> bool
   val isRel : Prelude.evar_map -> constr -> bool
@@ -827,6 +828,7 @@ sig
   val destConst : Prelude.evar_map -> constr -> Names.Constant.t * EInstance.t
   val destConstruct : Prelude.evar_map -> constr -> Names.constructor * EInstance.t
   val destFix : Evd.evar_map -> t -> (t, t) Term.pfixpoint
+  val destCast : Evd.evar_map -> t -> t * Term.cast_kind * t
 
   val mkConstruct : Names.constructor -> constr
 
@@ -866,6 +868,8 @@ sig
     val substl : constr list -> constr -> constr
     val lift : int -> constr -> constr
     val liftn : int -> int -> t -> t
+    val subst_var : Names.Id.t -> t -> t
+    val subst_vars : Names.Id.t list -> t -> t
   end
 
   val fresh_global :
@@ -907,6 +911,7 @@ val of_named_decl : (Term.constr, Term.types) Context.Named.Declaration.pt -> (c
   val mkConstU : Names.Constant.t * EInstance.t -> t
   val isProd : Evd.evar_map -> t -> bool
   val mkConstructUi : (Names.inductive * EInstance.t) * int -> t
+  val isLambda : Evd.evar_map -> t -> bool
 end
 
 module Mod_subst :
@@ -3262,10 +3267,11 @@ end
 module Proof_type :
 sig
   type goal = Evar.t
+  type rule = Proof_type.prim_rule =
+    | Cut of bool * bool * Names.Id.t * Term.types
+    | Refine of Term.constr
 
   type tactic = goal Evd.sigma -> goal list Evd.sigma
-
-  type rule = Proof_type.rule
 end
 
 module Redexpr :
@@ -3333,6 +3339,8 @@ sig
 
   val pf_nth_hyp_id : Proof_type.goal sigma -> int -> Names.Id.t
 
+  val sig_it : 'a sigma -> 'a
+
   module New :
   sig
     val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
@@ -3467,6 +3475,11 @@ sig
   val tclREPEAT : Proof_type.tactic -> Proof_type.tactic
   val tclORELSE        : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
   val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic
+  val tclIDTAC : Proof_type.tactic
+  val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+  val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic
+  val tclTRY : Proof_type.tactic -> Proof_type.tactic
+  val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic
 end
 
 module Termops :
@@ -4031,9 +4044,13 @@ sig
   val cache_term_by_tactic_then :
     opaque:bool -> ?goal_type:(EConstr.constr option) -> Names.Id.t ->
     Decl_kinds.goal_kind -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic
+  val apply_type : EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
+  val hnf_in_concl : unit Proofview.tactic
+  val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
 
   module New :
   sig
+    val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
     val reduce_after_refine : unit Proofview.tactic
   end
   module Simple :
@@ -4061,7 +4078,12 @@ sig
   val tclTHENS : tactic -> tactic list -> tactic
   val tclFIRST         : tactic list -> tactic
   val tclTHENFIRST     : tactic -> tactic -> tactic
+  val tclTHENLAST      : tactic -> tactic -> tactic
+  val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
+  val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
+  val tclSOLVE         : tactic list -> tactic
 
+  val onClause   : (Names.Id.t option -> tactic) -> Locus.clause -> tactic
   val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic
   val onLastHypId : (Names.Id.t -> tactic) -> tactic
   val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic
diff --git a/API/grammar_API.mli b/API/grammar_API.mli
index 350457f6c..44aae771f 100644
--- a/API/grammar_API.mli
+++ b/API/grammar_API.mli
@@ -177,6 +177,7 @@ sig
   val parse_string : 'a Gram.Entry.e -> string -> 'a
   val (!@) : Ploc.t -> Loc.t
   val set_command_entry : API.Vernacexpr.vernac_expr Gram.Entry.e -> unit
+  val to_coqloc : Ploc.t -> Loc.t
 end
 
 module CLexer :
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