Imported Upstream version 8.5~beta3+dfsg

9 files changed, 66 insertions, 44 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5151d2a1..c754f191 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for =
 	      let (argscs,_) = find_remaining_scopes pats [] g in
 	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
 	| NApp (NRef g,args) ->
-	      ensure_kind top loc g;
+	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
 	      let pats1,pats2 = List.chop nvars pats in
@@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for =
 	sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
       begin match sorted_fields with
 	| None -> RCPatAtom (loc, None)
-	| Some (_, head, pl) ->
+	| Some (n, head, pl) ->
+          let pl =
+            if !oldfashion_patterns then pl else
+            let pars = List.make n (CPatAtom (loc, None)) in
+            List.rev_append pars pl in
 	  match drop_syndef top env head pl with
 	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
@@ -1214,7 +1218,8 @@ let drop_notations_pattern looked_for =
 		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
 		 List.map2 (in_pat_sc env) argscs2 args)
     | NList (x,_,iter,terminator,lassoc) ->
-      let () = assert (List.is_empty args) in
+      if not (List.is_empty args) then user_err_loc
+        (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
 	 let (l,(scopt,subscopes)) = Id.Map.find x substlist in
@@ -1893,7 +1898,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err_loc (loc,"internalize", explain_internalization_error e)
 
-let interp_rawcontext_evars env evdref bl =
+let interp_rawcontext_evars env evdref k bl =
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
@@ -1913,12 +1918,12 @@ let interp_rawcontext_evars env evdref bl =
 	  | Some b ->
 	      let c = understand_judgment_tcc env evdref b in
 	      let d = (na, Some c.uj_val, c.uj_type) in
-		(push_rel d env, d::params, succ n, impls))
-      (env,[],1,[]) (List.rev bl)
+		(push_rel d env, d::params, n, impls))
+      (env,[],k+1,[]) (List.rev bl)
   in (env, par), impls
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) env evdref params =
+let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars env evdref bl in
+  let x = interp_rawcontext_evars env evdref shift bl in
   int_env, x
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 0d33d433..b671c988 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -95,7 +95,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list ->
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
-(** Main interpretation functions expecting evars to be all resolved *)
+(** Main interpretation functions, using type class inference,
+    expecting evars and pending problems to be all resolved *)
 
 val interp_constr : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> constr Evd.in_evar_universe_context
@@ -106,9 +107,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env ->
 val interp_type : env -> evar_map -> ?impls:internalization_env ->
   constr_expr -> types Evd.in_evar_universe_context
 
-(** Main interpretation function expecting evars to be all resolved *)
+(** Main interpretation function expecting all postponed problems to
+    be resolved, but possibly leaving evars. *)
 
-val interp_open_constr   : env -> evar_map -> constr_expr -> evar_map * constr
+val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
@@ -157,7 +159,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?global_level:bool -> ?impl_env:internalization_env ->
+  ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map ref -> local_binder list ->
   internalization_env * ((env * rel_context) * Impargs.manual_implicits)
 
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 02504c92..5ac718e3 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -54,15 +54,15 @@ let gen_reference_in_modules locstr dirs s =
   match these with
     | [x] -> x
     | [] ->
-	anomaly ~label:locstr (str ("cannot find "^s^
-	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	anomaly ~label:locstr (str "cannot find " ++ str s ++
+	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	prlist_with_sep pr_comma pr_dirpath dirs)
     | l ->
       anomaly ~label:locstr
-	(str ("ambiguous name "^s^" can represent ") ++
+	(str "ambiguous name " ++ str s ++ str " can represent " ++
 	   prlist_with_sep pr_comma
 	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-	   str (" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
 	   prlist_with_sep pr_comma pr_dirpath dirs)
 
 let gen_constant_in_modules locstr dirs s =
@@ -86,7 +86,8 @@ let check_required_library d =
      (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      error ("Library "^(DirPath.to_string dir)^" has to be required first.")
+      errorlabstrm "Coqlib.check_required_library"
+        (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e304725d..87f7a6d6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -245,21 +245,21 @@ let combine_params_freevar =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l
-    | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
+    | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let (loc, r, _ as clapp) = destClassAppExpl ty in
+      let (_, r, _, _ as clapp) = destClassAppExpl ty in
       let (loc, qid) = qualid_of_reference r in
       let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -267,7 +267,7 @@ let implicit_application env ?(allow_partial=true) f ty =
   in
     match is_class with
     | None -> ty, env
-    | Some ((loc, id, par), gr) ->
+    | Some ((loc, id, par, inst), gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
@@ -285,7 +285,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    CAppExpl (loc, (None, id, None), args), avoid
+	    CAppExpl (loc, (None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 818f7e9a..eee92898 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Globnames
 val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
-val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
@@ -28,7 +28,7 @@ val free_vars_of_binders :
   ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
-   order with the location of their first occurence *)
+   order with the location of their first occurrence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
   glob_constr -> (Id.t * Loc.t) list
diff --git a/interp/modintern.ml b/interp/modintern.ml
index bf0b2f98..35e73113 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,7 +62,7 @@ let transl_with_decl env = function
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
     let c, ectx = interp_constr env (Evd.from_env env) c in
-    let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in
+    let ctx = Evd.evar_context_universe_context ectx in
       WithDef (fqid,(c,ctx))
 
 let loc_of_module = function
diff --git a/interp/notation.ml b/interp/notation.ml
index 80db2cb3..d18b804b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -91,7 +91,9 @@ let declare_scope scope =
 (*    Flags.if_warn message ("Creating scope "^scope);*)
     scope_map := String.Map.add scope empty_scope !scope_map
 
-let error_unknown_scope sc = error ("Scope "^sc^" is not declared.")
+let error_unknown_scope sc =
+  errorlabstrm "Notation"
+    (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope scope =
   try String.Map.find scope !scope_map
@@ -186,23 +188,36 @@ let declare_delimiters scope key =
     | Some oldkey when String.equal oldkey key -> ()
     | Some oldkey ->
 	msg_warning
-	  (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
+	  (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope);
 	scope_map := String.Map.add scope newsc !scope_map
   end;
   try
     let oldscope = String.Map.find key !delimiters_map in
     if String.equal oldscope scope then ()
     else begin
-      msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope));
+      msg_warning (str "Hiding binding of key " ++ str key ++ str " to " ++ str oldscope);
       delimiters_map := String.Map.add key scope !delimiters_map
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
 
+let remove_delimiters scope =
+  let sc = find_scope scope in
+  let newsc = { sc with delimiters = None } in
+  match sc.delimiters with
+    | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+    | Some key ->
+       scope_map := String.Map.add scope newsc !scope_map;
+       try
+         let _ = ignore (String.Map.find key !delimiters_map) in
+         delimiters_map := String.Map.remove key !delimiters_map
+       with Not_found ->
+         assert false (* A delimiter for scope [scope] should exist *)
+
 let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
     user_err_loc
-    (loc, "find_delimiters", str ("Unknown scope delimiting key "^key^"."))
+    (loc, "find_delimiters", str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
 
@@ -317,8 +332,7 @@ let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
     user_err_loc (loc,"prim_token_interpreter",
-    str ("Cannot interpret in "^sc^" without requiring first module "
-    ^(List.last d)^"."))
+    str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
@@ -373,10 +387,9 @@ let declare_notation_interpretation ntn scopt pat df =
   let () =
     if String.Map.mem ntn sc.notations then
     let which_scope = match scopt with
-    | None -> ""
-    | Some _ -> " in scope " ^ scope in
-    let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in
-    msg_warning (strbrk message)
+    | None -> mt ()
+    | Some _ -> str " in scope " ++ str scope in
+    msg_warning (str "Notation " ++ str ntn ++ str " was already used" ++ which_scope)
   in
   let sc = { sc with notations = String.Map.add ntn (pat,df) sc.notations } in
   let () = scope_map := String.Map.add scope sc !scope_map in
@@ -452,7 +465,7 @@ let interp_notation loc ntn local_scopes =
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
-    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
+    (loc,"",str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
   List.map_append (fun key -> keymap_find key !notations_key_table)
@@ -783,9 +796,9 @@ let pr_scope_classes sc =
   let l = classes_of_scope sc in
   match l with
   | [] -> mt ()
-  | _ :: l ->
-    let opt_s = match l with [] -> "" | _ -> "es" in
-    hov 0 (str ("Bound to class" ^ opt_s) ++
+  | _ :: ll ->
+    let opt_s = match ll with [] -> mt () | _ -> str "es" in
+    hov 0 (str "Bound to class" ++ opt_s ++
       spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
 
 let pr_notation_info prglob ntn c =
diff --git a/interp/notation.mli b/interp/notation.mli
index 854c52b2..38bd5fc7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,6 +55,7 @@ val find_scope : scope_name -> scope
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
+val remove_delimiters : scope_name -> unit
 val find_delimiters_scope : Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 9be7abcf..d2709d5e 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -99,7 +99,7 @@ let verbose_compat kn def = function
       | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
       | _ -> str " is a compatibility notation"
     in
-    let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in
+    let since = str " since Coq > " ++ str (Flags.pr_version v) ++ str "." in
     act (pr_syndef kn ++ pp_def ++ since)
   | _ -> ()