Merge branch 'v8.5'

5 files changed, 65 insertions, 26 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b65ff73fe..e54a82c19 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -251,7 +251,7 @@ let declare_assumptions idl is_coe k (c,ctx) imps impl_is_on nl =
   in
   List.rev refs, status
 
-let do_assumptions (_, poly, _ as kind) nl l =
+let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
@@ -284,6 +284,44 @@ let do_assumptions (_, poly, _ as kind) nl l =
     in
       (subst'@subst, status' && status)) ([],true) l)
 
+let do_assumptions_bound_univs coe kind nl id pl c =
+  let env = Global.env () in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
+  let ty, impls = interp_type_evars_impls env evdref c in
+  let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
+  let ty = nf ty in
+  let vars = Universes.universes_of_constr ty in
+  let evd = Evd.restrict_universe_context !evdref vars in
+  let uctx = Evd.universe_context ?names:pl evd in
+  let uctx = Univ.ContextSet.of_context uctx in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) impls false nl id in
+  st
+
+let do_assumptions kind nl l = match l with
+| [coe, ([id, Some pl], c)] ->
+  let () = match kind with
+  | (Discharge, _, _) when Lib.sections_are_opened () ->
+    let loc = fst id in
+    let msg = Pp.str "Section variables cannot be polymorphic." in
+    user_err_loc (loc, "", msg)
+  | _ -> ()
+  in
+  do_assumptions_bound_univs coe kind nl id (Some pl) c
+| _ ->
+  let map (coe, (idl, c)) =
+    let map (id, univs) = match univs with
+    | None -> id
+    | Some _ ->
+      let loc = fst id in
+      let msg = Pp.str "Assumptions with bound universes can only be defined once at a time." in
+      user_err_loc (loc, "", msg)
+    in
+    (coe, (List.map map idl, c))
+  in
+  let l = List.map map l in
+  do_assumptions_unbound_univs kind nl l
+
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
 (* 3b| Mutual inductive definitions *)
@@ -500,12 +538,13 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
-  let evdref = ref Evd.(from_env env0) in
+  let pl = (List.hd indl).ind_univs in
+  let ctx = Evd.make_evar_universe_context env0 pl in
+  let evdref = ref Evd.(from_ctx ctx) in
   let _, ((env_params, ctx_params), userimpls) =
     interp_context_evars env0 evdref paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
-  let pl = (List.hd indl).ind_univs in
       
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter(fun (_,b,_) -> Option.is_empty b) ctx_params in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index f4d43ec53..b1e1d7d06 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -57,7 +57,7 @@ val declare_assumption : coercion_flag -> assumption_kind ->
   global_reference * Univ.Instance.t * bool
 
 val do_assumptions : locality * polymorphic * assumption_object_kind ->
-  Vernacexpr.inline -> simple_binder with_coercion list -> bool
+  Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
 (*   coercion_flag -> assumption_kind -> types Univ.in_universe_context_set ->  *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 076db5e11..d41ecebe0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -359,7 +359,8 @@ let get_int opt n =
 
 let get_host_port opt s =
   match CString.split ':' s with
-  | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+  | [host; portr; portw] ->
+       Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
   | ["stdfds"] -> Some Spawned.AnonPipe
   | _ ->
      prerr_endline ("Error: host:port or stdfds expected after option "^opt);
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index d2bd2c07b..836de042b 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -798,7 +798,7 @@ let solve_by_tac name evi t poly ctx =
   let entry = Term_typing.handle_entry_side_effects env entry in
   let body, eff = Future.force entry.Entries.const_entry_body in
   assert(Declareops.side_effects_is_empty eff);
-  let ctx' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
+  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx'
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 229f3acfd..d0e231b26 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -515,7 +515,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let kind = local, poly, kind in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
-      List.iter (fun lid ->
+      List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
   let status = do_assumptions kind nl l in
@@ -874,18 +874,7 @@ let vernac_set_used_variables e =
       errorlabstrm "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
-  let closure_l = List.map pi1 (set_used_variables l) in
-  let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in
-  let vars_of = Environ.global_vars_set in
-  let aux env entry (all_safe,rest as orig) =
-    match entry with
-    | (x,None,_) ->
-       if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) 
-    | (x,Some bo, ty) ->
-       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
-       if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest)
-       else (all_safe, (Loc.ghost,x) :: rest) in
-  let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in
+  let _, to_clear = set_used_variables l in
   vernac_solve
     SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false
 
@@ -1497,6 +1486,8 @@ let vernac_set_opacity locality (v,l) =
 
 let vernac_set_option locality key = function
   | StringValue s -> set_string_option_value_gen locality key s
+  | StringOptValue (Some s) -> set_string_option_value_gen locality key s
+  | StringOptValue None -> unset_option_value_gen locality key
   | IntValue n -> set_int_option_value_gen locality key n
   | BoolValue b -> set_bool_option_value_gen locality key b
 
@@ -1855,8 +1846,9 @@ let vernac_load interp fname =
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility *)
-let interp ?proof locality poly c =
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let interp ?proof ~loc locality poly c =
   prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* Done later in this file *)
@@ -2000,10 +1992,16 @@ let interp ?proof locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
-  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (None, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no"
+  | VernacProof (Some tac, None) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no";
+      vernac_set_end_tac tac
+  | VernacProof (None, Some l) ->
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes";
+      vernac_set_used_variables l
   | VernacProof (Some tac, Some l) -> 
+      Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes";
       vernac_set_end_tac tac; vernac_set_used_variables l
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
@@ -2155,8 +2153,9 @@ let interp ?(verbosely=true) ?proof (loc,c) =
         Obligations.set_program_mode isprogcmd;
         try
           vernac_timeout begin fun () ->
-          if verbosely then Flags.verbosely (interp ?proof locality poly) c
-                       else Flags.silently  (interp ?proof locality poly) c;
+          if verbosely
+            then Flags.verbosely (interp ?proof ~loc locality poly) c
+            else Flags.silently  (interp ?proof ~loc locality poly) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode
           end