diff options
| author | Jason Gross | 2018-07-24 13:06:03 -0400 |
|---|---|---|
| committer | Jason Gross | 2018-08-31 20:05:54 -0400 |
| commit | ebf453d4ae4e4f0312f3fd696da26c03671bc906 (patch) | |
| tree | 875586f7bf2013b57d4e19144d0d8653292c462f /plugins/syntax | |
| parent | d1460484d4804f953c8997eb7d1cf9d1384a82c9 (diff) | |
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
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/g_numeral.ml4 | 11 |
1 files changed, 6 insertions, 5 deletions
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 |