From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: 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.
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

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
-- 
cgit v1.2.3


From 8d69323dff6e1afd17a13dfa8a980e76acb44cdc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:35 +0200
Subject: Documenting how the recursive indices of a fixpoint are computed.

Also documenting how the implicit arguments by position are computed.
---
 intf/constrexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8e..a4a6eb9092 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 type notation = string
 
 type explicitation =
-  | ExplByPos of int * Id.t option
+  | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
 
 type binder_kind =
-- 
cgit v1.2.3