Removing internal support for accepting "{struct x}" and co in "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.

6 files changed, 11 insertions, 29 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e787e48bf1..74d0438dd4 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -553,7 +553,7 @@ let rec tmpp v loc =
       let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
       let str_id = Id.to_string id in
       (xmlDef str_dk str_id loc [pp_expr e])
-  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
+  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement) ], b) ->
       let str_tk = Kindops.string_of_theorem_kind tk in
       let str_id = Id.to_string id in
       (xmlThm str_tk str_id loc [pp_expr statement])
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 25d3c705f4..d62c639c2e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -209,7 +209,7 @@ type one_inductive_expr =
   plident * local_binder_expr list * constr_expr option * constructor_expr list
 
 type proof_expr =
-  plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option)
+  plident option * (local_binder_expr list * constr_expr)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 71b93439bc..6ede0490e4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -146,8 +146,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = pidentref; bl = binders; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = pidentref; bl = binders; ":"; c = lconstr ->
-          (Some id,(bl,c,None)) ] ->
-          VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false)
+          (Some id,(bl,c)) ] ->
+          VernacStartTheoremProof (thm, (Some id,(bl,c))::l, false)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index cfc2e48d11..d3b4007fbe 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -386,13 +386,12 @@ open Decl_kinds
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr def) def
     ++ prlist (pr_decl_notation pr_constr) ntn
 
-  let pr_statement head (idpl,(bl,c,guard)) =
+  let pr_statement head (idpl,(bl,c)) =
     assert (not (Option.is_empty idpl));
     let id, pl = Option.get idpl in
     hov 2
       (head ++ spc() ++ pr_lident id ++ pr_univs pl ++ spc() ++
          (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-         pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
          str":" ++ pr_spc_lconstr c)
 
   let pr_priority = function
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 409676276a..e7d1919ce0 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -88,25 +88,9 @@ let adjust_guardness_conditions const = function
 
 let find_mutually_recursive_statements thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls,annot)) ->
+    let inds = List.map (fun (id,(t,impls)) ->
       let (hyps,ccl) = decompose_prod_assum t in
       let x = (id,(t,impls)) in
-      match annot with
-      (* Explicit fixpoint decreasing argument is given *)
-      | Some (Some (_,id),CStructRec) ->
-          let i,b,typ = lookup_rel_id id hyps in
-          (match kind_of_term t with
-          | Ind ((kn,_ as ind), u) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
-              [ind,x,i],[]
-          | _ ->
-              error "Decreasing argument is not an inductive assumption.")
-      (* Unsupported cases *)
-      | Some (_,(CWfRec _|CMeasureRec _)) ->
-          error "Only structural decreasing is supported for mutual statements."
-      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
-      | None | Some (None, CStructRec) ->
       let whnf_hyp_hds = map_rel_context_in_env
         (fun env c -> fst (whd_all_stack env Evd.empty c))
         (Global.env()) hyps in
@@ -178,7 +162,7 @@ let find_mutually_recursive_statements thms =
     (finite,guard,None), ordered_inds
 
 let look_for_possibly_mutual_statements = function
-  | [id,(t,impls,None)] ->
+  | [id,(t,impls)] ->
       (* One non recursively proved theorem *)
       None,[id,(t,impls)],None
   | _::_ as thms ->
@@ -458,7 +442,7 @@ let start_proof_com ?inference_hook kind thms hook =
 		    | None -> Evd.from_env env0
 		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
   in
-  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+  let thms = List.map (fun (sopt,(bl,t)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     let flags = all_and_fail_flags in
@@ -467,8 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
+       (ids, imps @ lift_implicits (List.length ids) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca03ba3f3a..07066d983d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,7 +489,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
 	  start_proof_and_print (local,p,DefinitionBody k)
-	    [Some (lid,pl), (bl,t,None)] hook
+	    [Some (lid,pl), (bl,t)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
@@ -2077,7 +2077,7 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()