diff options
| author | Hugo Herbelin | 2018-09-28 18:40:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-28 18:51:02 +0200 |
| commit | 2ea68be1bf7b5977234957f8ad04fdaa0ce539a2 (patch) | |
| tree | e798ed949c909b949ae04b4fc29e59653a119077 /pretyping/indrec.mli | |
| parent | 0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (diff) | |
Functionalizing calls to the environment in Himsg.
This shall eventually allow to call Himsg at any point of the
execution, independently of the exact current global environment.
Diffstat (limited to 'pretyping/indrec.mli')
| -rw-r--r-- | pretyping/indrec.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index de9d3a0abf..91a5651f7f 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -20,7 +20,7 @@ type recursion_scheme_error = | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive -exception RecursionSchemeError of recursion_scheme_error +exception RecursionSchemeError of env * recursion_scheme_error (** Eliminations *) |