diff options
| author | Pierre-Marie Pédrot | 2019-02-17 14:27:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-17 14:27:26 +0100 |
| commit | a49077ef67b8e70696ecacc311fc3070d1b7b461 (patch) | |
| tree | 1d9adcfba5d77543a91140dbacbe975da00c213e /doc/plugin_tutorial | |
| parent | 9014e6544cb251f140636f774e95df4037d8d8f6 (diff) | |
| parent | ac7169182a970c33be2e33abd43be5bf19542e2c (diff) | |
Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index 1f636c531a..2949adde73 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -6,7 +6,7 @@ let simple_check1 value_with_constraints = (* The point of renaming is to make sure the bound names printed by Check can be re-used in `apply with` tactics that use bound names to refer to arguments. *) - let j = Termops.on_judgment EConstr.of_constr + let j = Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing (Global.env()) (EConstr.to_constr evd evalue)) in let {Environ.uj_type=x}=j in x |