From b0f8e09c3212fa96934817e7ca99465cd634f57c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 14:33:55 -0400
Subject: [interp] [numeral] Use cbv rather than vm

It is important to fully normalize the term, *including inductive
parameters of constructors*; see https://github.com/coq/coq/issues/9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.

Supersedes / closes #9655
---
 interp/notation.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index bc68d97bb8..cdc2594454 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -606,20 +606,18 @@ module PrimTokenNotation = struct
     At least [c] is known to be evar-free, since it comes from
     our own ad-hoc [constr_of_glob] or from conversions such
     as [coqint_of_rawnum].
-*)
 
-let eval_constr env sigma (c : Constr.t) =
-  let c = EConstr.of_constr c in
-  let sigma,t = Typing.type_of env sigma c in
-  let c' = Vnorm.cbv_vm env sigma c t in
-  EConstr.Unsafe.to_constr c'
+    It is important to fully normalize the term, *including inductive
+    parameters of constructors*; see
+    https://github.com/coq/coq/issues/9840 for details on what goes
+    wrong if this does not happen, e.g., from using the vm rather than
+    cbv.
+*)
 
-(* For testing with "compute" instead of "vm_compute" :
 let eval_constr env sigma (c : Constr.t) =
   let c = EConstr.of_constr c in
   let c' = Tacred.compute env sigma c in
   EConstr.Unsafe.to_constr c'
-*)
 
 let eval_constr_app env sigma c1 c2 =
   eval_constr env sigma (mkApp (c1,[| c2 |]))
-- 
cgit v1.2.3


From 67e93e9ff5e5b1723ff62da8a82782e5030b5721 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 15:00:00 -0400
Subject: [numeral] Add a case for IndRef in constr_of_glob

Fixes #9840
---
 interp/notation.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index cdc2594454..b5e91b17e6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -632,6 +632,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with
   | Glob_term.GRef (ConstructRef c, _) ->
       let sigma,c = Evd.fresh_constructor_instance env sigma c in
       sigma,mkConstructU c
+  | Glob_term.GRef (IndRef c, _) ->
+      let sigma,c = Evd.fresh_inductive_instance env sigma c in
+      sigma,mkIndU c
   | Glob_term.GApp (gc, gcl) ->
       let sigma,c = constr_of_glob env sigma gc in
       let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
-- 
cgit v1.2.3


From 73c924d3d4bcc22a179cb974603f9072599ebb77 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 31 Mar 2019 15:35:21 -0400
Subject: Update numeral notation printing doc

Fixes #9844
---
 interp/notation.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index b5e91b17e6..2765661749 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -626,7 +626,13 @@ exception NotAValidPrimToken
 
 (** The uninterp function below work at the level of [glob_constr]
     which is too low for us here. So here's a crude conversion back
-    to [constr] for the subset that concerns us. *)
+    to [constr] for the subset that concerns us.
+
+    Note that if you update [constr_of_glob], you should update the
+    corresponding numeral notation *and* string notation doc in
+    doc/sphinx/user-extensions/syntax-extensions.rst that describes
+    what it means for a term to be ground / to be able to be
+    considered for parsing. *)
 
 let rec constr_of_glob env sigma g = match DAst.get g with
   | Glob_term.GRef (ConstructRef c, _) ->
-- 
cgit v1.2.3