diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:06:42 +0000 |
| commit | 1117d2e4a00debfbfa0157cc3e780916df72c26b (patch) | |
| tree | d8713b1126725f216e1d5ff1dcc9561d84069145 /print.mli | |
| parent | 17564e4922acda6b72bf39de7a8c23ed0c0178f6 (diff) | |
New upstream version 8.6
Diffstat (limited to 'print.mli')
| -rw-r--r-- | print.mli | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -10,7 +10,7 @@ tactic. *) -(** The main printing function. {!print} uses the [Term.rel_context] +(** The main printing function. {!print} uses the rel-context to rename the variables, and rebuilds raw Coq terms (for the given context, and the terms in the environment). In order to do so, it requires the information gathered by the {!Theory.Trans} module.*) @@ -18,6 +18,6 @@ val print : Coq.Relation.t -> Theory.Trans.ir -> (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m -> - Context.rel_context -> + Context.Rel.t -> Proof_type.tactic |