diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/plugin_tutorial/tuto1/src/simple_check.ml | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 9 |
2 files changed, 10 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 diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 4f486a777d..c134563efe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1162,6 +1162,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ |