diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-23 03:40:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-01 16:11:55 +0200 |
| commit | cf906af70f5c48cab99bd89047af0b2831850cf1 (patch) | |
| tree | 63e61ffc689a73ccc3d1ed53276234e4740f5df7 /printing/printer.ml | |
| parent | cabce8ae233040c2365bfd8bd1f478676fcade33 (diff) | |
Printing goals does not evar-normalizes beforehand anymore.
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 0d8168be9..e9d104b49 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -479,7 +479,8 @@ let pr_transparent_state (ids, csts) = (* display complete goal *) let default_pr_goal gs = - let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in + let g = sig_it gs in + let sigma = project gs in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = |