diff options
| -rw-r--r-- | interp/notation.ml | 14 |
1 files changed, 6 insertions, 8 deletions
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 |])) |