plugin that compiles with 8.5

mathcomp/ssreflect/plugin/trunk/ssreflect.ml4

@@ -66,6 +66,9 @@ open Notation_ops
 open Locus
 open Locusops
 
+open Compat
+open Tok
+
 open Ssrmatching
 
 
@@ -862,7 +865,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   let evplist = 
     let depev = List.fold_left (fun evs (_,(_,t,_)) -> 
         Intset.union evs (Evarutil.undefined_evars_of_term sigma t)) Intset.empty evlist in
-    List.filter (fun i,(_,_,b) -> b && Intset.mem i depev) evlist in
+    List.filter (fun (i,(_,_,b)) -> b && Intset.mem i depev) evlist in
   let evlist, evplist, sigma = 
     if evplist = [] then evlist, [], sigma else
     List.fold_left (fun (ev, evp, sigma) (i, (_,t,_) as p) ->
@@ -1835,14 +1838,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with
 
 let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind
 
-let id_of_Cterm t = match id_of_cpattern t with
-  | Some x -> x
-  | None -> loc_error (loc_of_cpattern t) "Only identifiers are allowed here"
-let ssrhyp_of_ssrterm = function
-  | k, (_, Some c) as o ->
-     SsrHyp (constr_loc c, id_of_Cterm (cpattern_of_term o)), String.make 1 k
-  | _, (_, None) -> assert false
-
 (* terms *)
 let pr_ssrterm _ _ _ = pr_term
 let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c
@@ -2006,7 +2001,7 @@ let check_wgen_uniq gens =
   check [] ids
 
 let pf_clauseids gl gens clseq =
-  let keep_clears = List.map (fun x, _ -> x, None) in
+  let keep_clears = List.map (fun (x, _) -> x, None) in
   if gens <> [] then (check_wgen_uniq gens; gens) else
   if clseq <> InAll && clseq <> InAllHyps then keep_clears gens else
   Errors.error "assumptions should be named explicitly"
@@ -2640,7 +2635,7 @@ END
 let reject_ssrhid strm =
   match Compat.get_tok (stream_nth 0 strm) with
   | Tok.KEYWORD "[" ->
-      (match Compat.get_tok (stream_nth 0 strm) with
+      (match Compat.get_tok (stream_nth 1 strm) with
       | Tok.KEYWORD ":" -> raise Stream.Failure
       | _ -> ())
   | _ -> ()
@@ -3160,7 +3155,7 @@ let check_seqtacarg dir arg = match snd arg, dir with
     loc_error loc "expected \"first\""
   | _, _ -> arg
 
-let ssrorelse = Gram.Entry.create "ssrorelse"
+let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
@@ -3697,10 +3692,12 @@ ARGUMENT EXTEND ssrmovearg TYPED AS ssrarg PRINTED BY pr_ssrarg
 END
 
 let viewmovetac_aux clear name_ref (_, vl as v) _ gen ist gl =
-  let cl, c, clr, gl = pf_interp_gen ist gl false gen in
+  let cl, c, clr, gl, gen_pat =
+    let _, gen_pat, a, b, c, ucst = pf_interp_gen_aux ist gl false gen in
+    a, b ,c, pf_merge_uc ucst gl, gen_pat in
   let cl, c, gl = if vl = [] then cl, c, gl else pf_with_view ist gl v cl c in
   let clr = if clear then clr else [] in
-  name_ref := (match id_of_cpattern (snd gen) with Some id -> id | _ -> top_id);
+  name_ref := (match id_of_pattern gen_pat with Some id -> id | _ -> top_id);
   genclrtac cl [c] clr gl
 
 let () = move_top_with_view := 
@@ -5763,7 +5760,8 @@ let ssrabstract ist gens (*last*) gl =
     let fire gl t = Reductionops.nf_evar (project gl) t in
     let abstract, gl = pf_mkSsrConst "abstract" gl in
     let abstract_key, gl = pf_mkSsrConst "abstract_key" gl in
-    let id = mkVar (Option.get (id_of_cpattern cid)) in
+    let cid_interpreted = interp_cpattern ist gl cid None in
+    let id = mkVar (Option.get (id_of_pattern cid_interpreted)) in
     let idty, args_id = examine_abstract id gl in
     let abstract_n = args_id.(1) in
     let abstract_proof = pf_find_abstract_proof true gl abstract_n in 
@@ -5807,7 +5805,7 @@ let ssrabstract ist gens (*last*) gl =
   in
   let introback ist (gens, _) =
     introstac ~ist
-      (List.map (fun (_,cp) -> match id_of_cpattern cp with
+      (List.map (fun (_,cp) -> match id_of_pattern (interp_cpattern ist gl cp None) with
         | None -> IpatAnon
         | Some id -> IpatId id)
         (List.tl (List.hd gens))) in
@@ -6058,9 +6056,6 @@ END
 
 (** Canonical Structure alias *)
 
-let def_body : Vernacexpr.definition_expr Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find (Obj.magic gallina_ext) "vernac:def_body") in
-
 GEXTEND Gram
   GLOBAL: gallina_ext;
 
@@ -6071,7 +6066,7 @@ GEXTEND Gram
       | IDENT "Canonical"; ntn = Prim.by_notation ->
 	  Vernacexpr.VernacCanonical (ByNotation ntn)
       | IDENT "Canonical"; qid = Constr.global;
-          d = def_body ->
+          d = G_vernac.def_body ->
           let s = coerce_reference_to_id qid in
 	  Vernacexpr.VernacDefinition
 	    ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure),
@@ -6093,18 +6088,11 @@ END
 (* Coq v8.3 defines "by" as a keyword, some hacks are not needed any   *)
 (* longer and thus comment out. Such comments are marked with v8.3     *)
 
-let tac_ent = List.fold_left Grammar.Entry.find (Obj.magic simple_tactic) in
-let hypident_ent =
-  tac_ent ["clause_dft_all"; "in_clause"; "hypident_occ"; "hypident"] in
-let id_or_meta : Obj.t Gram.Entry.e = Obj.magic
-   (Grammar.Entry.find hypident_ent "id_or_meta") in
-let hypident : (Obj.t * hyp_location_flag) Gram.Entry.e =
-   Obj.magic hypident_ent in
 GEXTEND Gram
-  GLOBAL: hypident;
-hypident: [
-  [ "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id, InHypTypeOnly
-  | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id, InHypValueOnly
+  GLOBAL: Tactic.hypident;
+  Tactic.hypident: [
+  [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly
+  | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly
   ] ];
 END
 
@@ -6118,13 +6106,9 @@ hloc: [
   ] ];
 END
 
-let constr_eval
- : (Constrexpr.constr_expr,Obj.t,Obj.t) Genredexpr.may_eval Gram.Entry.e
- = Obj.magic (Grammar.Entry.find (Obj.magic constr_may_eval) "constr_eval")
-
 GEXTEND Gram
-  GLOBAL: constr_eval;
-  constr_eval: [
+  GLOBAL: Tactic.constr_eval;
+  Tactic.constr_eval: [
     [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ]
   ];
 END

mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4

@@ -1059,6 +1059,10 @@ let interp_pattern ist gl red redty =
 let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;;
 let interp_rpattern ist gl red = interp_pattern ist gl red None;;
 
+let id_of_pattern = function
+  | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None)
+  | _ -> None
+
 (* The full occurrence set *)
 let noindex = Some(false,[])
 

mathcomp/ssreflect/plugin/trunk/ssrmatching.mli

@@ -3,6 +3,7 @@
 open Genarg
 open Tacexpr
 open Environ
+open Tacmach
 open Evd
 open Proof_type
 open Term
@@ -60,15 +61,15 @@ val redex_of_pattern :
 (** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl]*)
 val interp_rpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   rpattern ->
     pattern
 
 (** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat]
     in the current [Ltac] interpretation signature [ise] and tactic input [gl].
     [ty] is an optional type for the redex of [cpat] *)
 val interp_cpattern :
-  Tacinterp.interp_sign -> goal Tacmach.sigma ->
+  Tacinterp.interp_sign -> goal sigma ->
   cpattern -> glob_constr_and_expr option ->
     pattern
 
@@ -191,8 +192,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 Tacmach.sigma -> occ -> evar_map * constr -> constr * constr
+val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr
 
 (* 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
@@ -215,13 +215,13 @@ val assert_done : 'a option ref -> 'a
     In case of failure they raise [NoMatch] *)
 
 val unify_HO : env -> evar_map -> constr -> constr -> evar_map
-val pf_unify_HO : goal Tacmach.sigma -> constr -> constr -> goal Tacmach.sigma
+val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma
 
 (** Some more low level functions needed to implement the full SSR language
     on top of the former APIs *)
 val tag_of_cpattern : cpattern -> char
 val loc_of_cpattern : cpattern -> Loc.t
-val id_of_cpattern : cpattern -> Names.variable option
+val id_of_pattern : pattern -> Names.variable option
 val is_wildcard : cpattern -> bool
 val cpattern_of_id : Names.variable -> cpattern
 val cpattern_of_id : Names.variable -> cpattern