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

---
 interp/implicit_quantifiers.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 58df9abc..4f3037b1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -17,12 +17,14 @@ open Glob_term
 open Constrexpr
 open Libnames
 open Typeclasses
-open Typeclasses_errors
 open Pp
 open Libobject
 open Nameops
 open Context.Rel.Declaration
 
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *)
+let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
+
 module RelDecl = Context.Rel.Declaration
 (*i*)
 
@@ -51,14 +53,14 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
 
-let in_generalizable : bool * Misctypes.lident list option -> obj =
+let in_generalizable : bool * lident list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
     classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
   }
 
-let declare_generalizable local gen =
+let declare_generalizable ~local gen =
  Lib.add_anonymous_leaf (in_generalizable (local, gen))
 
 let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
@@ -94,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
     else l
   in
   let rec aux bdvars l c = match CAst.(c.v) with
-    | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) ->
-        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | CRef (qid,_) when qualid_is_ident qid ->
+      found c.CAst.loc (qualid_basename qid) bdvars l
+    | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when
+        qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) ->
+        Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c
     | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
@@ -194,7 +198,7 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, decl) ->
     let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid)
+      (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid)
 
 let destClassApp cl =
   let open CAst in
@@ -216,9 +220,8 @@ let destClassAppExpl cl =
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
-      let qid = qualid_of_reference r in
-      let gr = Nametab.locate qid.CAst.v in
+      let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in
+      let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
     with Not_found -> None
   in
@@ -238,7 +241,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	      let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
 	      let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
 		if not (Int.equal needlen applen) then
-		  Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+                  mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-- 
cgit v1.2.3