diff options
Diffstat (limited to 'plugins/extraction/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 3a4ba0b34..ec39a2eae 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -29,7 +29,7 @@ val extract_fixpoint : val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type |