Merge origin/v8.5 into trunk

Did some manual merge in tactics/tactics.ml.

8 files changed, 48 insertions, 29 deletions

diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index e4aa69353d..16006a6adf 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -312,12 +312,13 @@ Conversely, to skip the printing of coercions, use
  {\tt Unset Printing Coercions}.
 By default, coercions are not printed.
 
-\asubsection{\tt Set Printing Coercion {\qualid}.}
-\optindex{Printing Coercion}
+\asubsection{\tt Add Printing Coercion {\qualid}.}
+\comindex{Add Printing Coercion}
+\comindex{Remove Printing Coercion}
 
 This command forces coercion denoted by {\qualid} to be printed.
 To skip the printing of coercion {\qualid}, use
- {\tt Unset Printing Coercion {\qualid}}.
+ {\tt Remove Printing Coercion {\qualid}}.
 By default, a coercion is never printed.
  
 \asection{Classes as Records}
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 23320daefb..d9aed87edc 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -117,18 +117,18 @@ let is_unit constrsinfos =
    | [] -> (* type without constructors *) true
    | _ -> false
 
-let infos_and_sort env ctx t =
-  let rec aux env ctx t max =
+let infos_and_sort env t =
+  let rec aux env t max =
     let t = whd_betadeltaiota env t in
       match kind_of_term t with
       | Prod (name,c1,c2) ->
         let varj = infer_type env c1 in
 	let env1 = Environ.push_rel (name,None,varj.utj_val) env in
 	let max = Universe.sup max (univ_of_sort varj.utj_type) in
-	  aux env1 ctx c2 max
+	  aux env1 c2 max
     | _ when is_constructor_head t -> max
     | _ -> (* don't fail if not positive, it is tested later *) max
-  in aux env ctx t Universe.type0m
+  in aux env t Universe.type0m
 
 (* Computing the levels of polymorphic inductive types
 
@@ -153,14 +153,14 @@ let infos_and_sort env ctx t =
 (* This (re)computes informations relevant to extraction and the sort of an
    arity or type constructor; we do not to recompute universes constraints *)
 
-let infer_constructor_packet env_ar_par ctx params lc =
+let infer_constructor_packet env_ar_par params lc =
   (* type-check the constructors *)
   let jlc = List.map (infer_type env_ar_par) lc in
   let jlc = Array.of_list jlc in
   (* generalize the constructor over the parameters *)
   let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in
   (* compute the max of the sorts of the products of the constructors types *)
-  let levels = List.map (infos_and_sort env_ar_par ctx) lc in
+  let levels = List.map (infos_and_sort env_ar_par) lc in
   let isunit = is_unit levels in
   let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in
   let level = List.fold_left (fun max l -> Universe.sup max l) min levels in
@@ -266,8 +266,7 @@ let typecheck_inductive env mie =
     List.fold_right2
       (fun ind arity_data inds ->
 	 let (lc',cstrs_univ) =
-	   infer_constructor_packet env_ar_par ContextSet.empty
-	     params ind.mind_entry_lc in
+	   infer_constructor_packet env_ar_par params ind.mind_entry_lc in
 	 let consnames = ind.mind_entry_consnames in
 	 let ind' = (arity_data,consnames,lc',cstrs_univ) in
 	   ind'::inds)
@@ -342,7 +341,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor
+  | LocalNotConstructor of rel_context * constr list
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -353,7 +352,7 @@ exception IllFormedInd of ill_formed_ind
 
 let mind_extract_params = decompose_prod_n_assum
 
-let explain_ind_err id ntyp env nbpar c nargs err =
+let explain_ind_err id ntyp env nbpar c err =
   let (lpar,c') = mind_extract_params nbpar c in
   match err with
     | LocalNonPos kt ->
@@ -361,9 +360,11 @@ let explain_ind_err id ntyp env nbpar c nargs err =
     | LocalNotEnoughArgs kt ->
 	raise (InductiveError
 		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
-    | LocalNotConstructor ->
+    | LocalNotConstructor (paramsctxt,args)->
+        let nparams = rel_context_nhyps paramsctxt in
 	raise (InductiveError
-		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
+		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
+                                  List.length args - nparams)))
     | LocalNonPar (n,i,l) ->
 	raise (InductiveError
 		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
@@ -587,7 +588,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
                 begin match hd with
                 | Rel j when Int.equal j (n + ntypes - i - 1) ->
                   check_correct_par ienv hyps (ntypes - i) largs
-                | _ -> raise (IllFormedInd LocalNotConstructor)
+                | _ -> raise (IllFormedInd (LocalNotConstructor(hyps,largs)))
                 end
               else
                 if not (List.for_all (noccur_between n ntypes) largs)
@@ -603,7 +604,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
           try
 	    check_constructors ienv true nmr rawc
           with IllFormedInd err ->
-	    explain_ind_err id (ntypes-i) env lparams c nargs err)
+	    explain_ind_err id (ntypes-i) env lparams c err)
       (Array.of_list lcnames) indlc
   in
   let irecargs = Array.map snd irecargs_nmr
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0714c93b4f..156c9a2772 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,13 +1251,18 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
+let report_anomaly _ =
+  let e = UserError ("", Pp.str "Conversion test raised an anomaly") in
+  let e = Errors.push e in
+  iraise e
+
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
     let _ = f ~evars reds env (Evd.universes sigma) x y in
     true
   with Reduction.NotConvertible -> false
-    | e when is_anomaly e -> error "Conversion test raised an anomaly"
+    | e when is_anomaly e -> report_anomaly e
 
 let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv_universes reds env sigma
 let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq_universes reds env sigma
@@ -1275,7 +1280,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
     try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false
     | Univ.UniverseInconsistency _ -> false
-    | e when is_anomaly e -> error "Conversion test raised an anomaly"
+    | e when is_anomaly e -> report_anomaly e
 
 let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
@@ -1316,7 +1321,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
   with
   | Reduction.NotConvertible -> sigma, false
   | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
-  | e when is_anomaly e -> error "Conversion test raised an anomaly"
+  | e when is_anomaly e -> report_anomaly e
 
 let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
       Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index fea0432aea..a688b94879 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -16,7 +16,7 @@ type 'a focus =
 
 (** Type of tactics potentially goal-dependent. If it contains a [Depends],
     then the length of the inner list is guaranteed to be the number of
-    currently focussed goals. Otherwise it means the tactic does not depends
+    currently focussed goals. Otherwise it means the tactic does not depend
     on the current set of focussed goals. *)
 type 'a t = 'a focus Proofview.tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 936c5988f6..221c661b21 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -179,7 +179,7 @@ let unsafe_intro env store (id, c, t) b =
     let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar id) b in
-    let sigma, ev = new_evar_instance nctx sigma nb ~store ninst in
+    let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
     Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
   end }
 
@@ -1868,7 +1868,7 @@ let clear_body ids =
     in
     check_hyps <*> check_concl <*>
     Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-      Evarutil.new_evar env sigma concl
+      Evarutil.new_evar env sigma ~principal:true concl
     end }
   end }
 
@@ -2383,8 +2383,14 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let t = match ty with Some t -> t | _ -> typ_of env sigma c in
-    let Sigma ((newcl, eq_tac), sigma, p) = match with_eq with
+    let Sigma (t, sigma, p) = match ty with
+    | Some t -> Sigma.here t sigma
+    | None ->
+      let t = typ_of env sigma c in
+      let sigma, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env (Sigma.to_evar_map sigma) t in
+      Sigma.Unsafe.of_pair (c, sigma)
+    in
+    let Sigma ((newcl, eq_tac), sigma, q) = match with_eq with
       | Some (lr,(loc,ido)) ->
           let heq = match ido with
             | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
@@ -2415,7 +2421,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty =
         Tacticals.New.tclMAP convert_hyp_no_check depdecls;
         eq_tac ]
     in
-    Sigma (tac, sigma, p)
+    Sigma (tac, sigma, p +> q)
   end }
 
 let insert_before decls lasthyp env =
@@ -2645,7 +2651,7 @@ let new_generalize_gen_let lconstr =
     in
     let tac =
 	Proofview.Refine.refine { run = begin fun sigma ->
-          let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in
+          let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in
           Sigma ((applist (ev, args)), sigma, p)
 	end }
     in
diff --git a/test-suite/bugs/closed/4404.v b/test-suite/bugs/closed/4404.v
new file mode 100644
index 0000000000..27b43a61d4
--- /dev/null
+++ b/test-suite/bugs/closed/4404.v
@@ -0,0 +1,4 @@
+Inductive Foo : Type -> Type := foo A : Foo A.
+Goal True.
+  remember Foo.
+
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 483a9ea792..52e1e0ed01 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,5 @@
 Existential 1 =
-?Goal0 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+?Goal1 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
 Existential 2 =
 ?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
-Existential 3 = ?e : [q : nat  n : nat  m : nat |- n = ?y] 
+Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 83a33f75dc..59cd25cd76 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -97,6 +97,7 @@ Abort.
 
 Goal exists x, S x = S 0.
 eexists.
+Show x.  (* Incidentally test Show on a named goal *)
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S 0).
 Abort.
@@ -105,6 +106,7 @@ Goal exists x, S 0 = S x.
 eexists.
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
+[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.