From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 22 May 2018 00:07:26 +0200
Subject: [api] Misctypes removal: several moves:

- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
---
 plugins/ssr/ssrparser.ml4 | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'plugins/ssr/ssrparser.ml4')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index fbfbdb1108..9d7fc254c4 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -29,6 +29,8 @@ open Extraargs
 open Ppconstr
 
 open Misctypes
+open Namegen
+open Tactypes
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
@@ -543,7 +545,7 @@ END
 
 let remove_loc x = x.CAst.v
 
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
   let rec ipat_of_intro_pattern = function
     | IntroNaming (IntroIdentifier id) -> IPatId id
     | IntroAction IntroWildcard -> IPatAnon Drop
@@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist)
 
 let interp_intro_pattern = interp_wit wit_intro_pattern
 
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
  try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
  with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
 
 let get_intro_id = function
   | IntroNaming (IntroIdentifier id) -> id
   | _ -> assert false
 
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
   let {CAst.loc=loc;v=ipat} = ipat in
   match ipat with
   | IntroNaming (IntroIdentifier id) ->
@@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
   | IntroForthcoming _ -> 
     (* As in ipat_of_intro_pattern, was unable to determine which kind
       of ipat interp_introid could return [HH] *) assert false
-)
 
 (* We interp the ipat using the standard ltac machinery for ids, since
  * we have no clue what a name could be bound to (maybe another ipat) *)
@@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = CCast (c, CastConv t) } ->
+  | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h, 
     { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
 
 let mkFwdVal fk c = ((fk, []), c)
 let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
 
 let same_ist { interp_env = x } { interp_env = y } =
   match x,y with
@@ -1210,8 +1210,8 @@ let push_binders c2 bs =
   | [] -> c
   | _ -> anomaly "binder not a lambda nor a let in" in
   match c2 with
-  | { loc; v = CCast (ct, CastConv cty) } ->
-      CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+  | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+      CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
-- 
cgit v1.2.3


From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 1 Jun 2018 02:37:15 +0200
Subject: [api] Remove Misctypes.

We move the last 3 types to more adequate places.
---
 plugins/ssr/ssrparser.ml4 | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/ssr/ssrparser.ml4')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 9d7fc254c4..352f88bb35 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -22,13 +22,13 @@ open Libnames
 open Tactics
 open Tacmach
 open Util
+open Locus
 open Tacexpr
 open Tacinterp
 open Pltac
 open Extraargs
 open Ppconstr
 
-open Misctypes
 open Namegen
 open Tactypes
 open Decl_kinds
@@ -303,24 +303,24 @@ END
 
 
 let pr_index = function
-  | Misctypes.ArgVar {CAst.v=id} -> pr_id id
-  | Misctypes.ArgArg n when n > 0 -> int n
+  | ArgVar {CAst.v=id} -> pr_id id
+  | ArgArg n when n > 0 -> int n
   | _ -> mt ()
 let pr_ssrindex _ _ _ = pr_index
 
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
 
 let check_index ?loc i =
   if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
 let mk_index ?loc = function
-  | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+  | ArgArg i -> ArgArg (check_index ?loc i)
   | iv -> iv
 
 let interp_index ist gl idx =
   Tacmach.project gl,
   match idx with
-  | Misctypes.ArgArg _ -> idx
-  | Misctypes.ArgVar id ->
+  | ArgArg _ -> idx
+  | ArgVar id ->
     let i =
       try
         let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -338,7 +338,7 @@ let interp_index ist gl idx =
         | None -> raise Not_found
         end end
     with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
-    Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+    ArgArg (check_index ?loc:id.CAst.loc i)
 
 open Pltac
 
-- 
cgit v1.2.3