From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/ltac/taccoerce.ml | 38 ++++++++++++++++++++------------------
 1 file changed, 20 insertions(+), 18 deletions(-)

(limited to 'plugins/ltac/taccoerce.ml')

diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 3812a2ba..026c00b8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -12,9 +12,11 @@ open Util
 open Names
 open Constr
 open EConstr
-open Misctypes
+open Namegen
+open Tactypes
 open Genarg
 open Stdarg
+open Tacarg
 open Geninterp
 open Pp
 
@@ -163,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v =
 (* Interprets, if possible, a constr to an identifier which may not
    be fresh but suitable to be given to the fresh tactic. Works for
    vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh env sigma v =
-let g = sigma in
+let coerce_to_ident_not_fresh sigma v =
 let id_of_name = function
   | Name.Anonymous -> Id.of_string "x"
   | Name.Name x -> x in
@@ -181,9 +182,9 @@ let id_of_name = function
     | Some c ->
        match EConstr.kind sigma c with
        | Var id -> id 
-       | Meta m -> id_of_name (Evd.meta_name g m)
+       | Meta m -> id_of_name (Evd.meta_name sigma m)
        | Evar (kn,_) ->
-        begin match Evd.evar_ident kn g with
+        begin match Evd.evar_ident kn sigma with
         | None -> fail ()
         | Some id -> id
         end
@@ -197,15 +198,16 @@ let id_of_name = function
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Sort s ->
-	  begin
+          begin
 	    match ESorts.kind sigma s with
-	    | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
-	    | Sorts.Type _ -> Label.to_id (Label.make "Type")
-	  end
+            | Sorts.Prop -> Label.to_id (Label.make "Prop")
+            | Sorts.Set -> Label.to_id (Label.make "Set")
+            | Sorts.Type _ -> Label.to_id (Label.make "Type")
+          end
        | _ -> fail()
 
 
-let coerce_to_intro_pattern env sigma v =
+let coerce_to_intro_pattern sigma v =
   if has_type v (topwit wit_intro_pattern) then
     (out_gen (topwit wit_intro_pattern) v).CAst.v
   else if has_type v (topwit wit_var) then
@@ -218,8 +220,8 @@ let coerce_to_intro_pattern env sigma v =
       IntroNaming (IntroIdentifier (destVar sigma c))
   | _ -> raise (CannotCoerceTo "an introduction pattern")
 
-let coerce_to_intro_pattern_naming env sigma v =
-  match coerce_to_intro_pattern env sigma v with
+let coerce_to_intro_pattern_naming sigma v =
+  match coerce_to_intro_pattern sigma v with
   | IntroNaming pat -> pat
   | _ -> raise (CannotCoerceTo "a naming introduction pattern")
 
@@ -252,7 +254,7 @@ let coerce_to_constr env v =
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
-let coerce_to_uconstr env v =
+let coerce_to_uconstr v =
   if has_type v (topwit wit_uconstr) then
     out_gen (topwit wit_uconstr) v
   else
@@ -296,11 +298,11 @@ let coerce_to_constr_list env v =
     List.map map l
   | None -> raise (CannotCoerceTo "a term list")
 
-let coerce_to_intro_pattern_list ?loc env sigma v =
+let coerce_to_intro_pattern_list ?loc sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
+    let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
     List.map map l
 
 let coerce_to_hyp env sigma v =
@@ -325,7 +327,7 @@ let coerce_to_hyp_list env sigma v =
   | None -> raise (CannotCoerceTo "a variable list")
 
 (* Interprets a qualified name *)
-let coerce_to_reference env sigma v =
+let coerce_to_reference sigma v =
   match Value.to_constr v with
   | Some c ->
     begin
@@ -353,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v =
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env sigma v =
+let coerce_to_decl_or_quant_hyp sigma v =
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
@@ -365,7 +367,7 @@ let coerce_to_int_or_var_list v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an int list")
   | Some l ->
-    let map n = ArgArg (coerce_to_int n) in
+    let map n = Locus.ArgArg (coerce_to_int n) in
     List.map map l
 
 (** Abstract application, to print ltac functions *)
-- 
cgit v1.2.3