From ebf453d4ae4e4f0312f3fd696da26c03671bc906 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 24 Jul 2018 13:06:03 -0400
Subject: Update doc and test-suite after supporting univ poly

Also make `Check S` no longer anomaly

Add a couple more test cases for numeral notations

Also add another possibly-confusing error message to the doc.

Respond to Hugo's doc request with Zimmi48's suggestion

From https://github.com/coq/coq/pull/8064/files#r204191608
---
 plugins/syntax/g_numeral.ml4 | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index 1d2d47fbaa..a097adec24 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -36,13 +36,14 @@ open Constr
 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
+  let c' = Vnorm.cbv_vm env sigma c t in
   EConstr.Unsafe.to_constr c'
 
 (* For testing with "compute" instead of "vm_compute" :
-let eval_constr (c : constr) =
- let (sigma, env) = Lemmas.get_current_context () in
- Tacred.compute env sigma c
+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 =
@@ -325,7 +326,7 @@ let uninterp o (Glob_term.AnyGlobConstr n) =
     | UInt _ -> Some (rawnum_of_coquint c, true)
     | Z _ -> Some (big2raw (bigint_of_z c))
   with
-  | Type_errors.TypeError _ -> None (* cf. eval_constr_app *)
+  | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *)
   | NotANumber -> None (* all other functions except big2raw *)
 
 (* Here we only register the interp and uninterp functions
-- 
cgit v1.2.3