diff options
| author | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
| commit | fcba5e87be13bc5a5374fe274476cd4d5c45f058 (patch) | |
| tree | 14707fa1bd939458f553b1baaf35becda2267675 /tactics/eauto.ml | |
| parent | 69daead8ae18d55ee445a918865ea2adf59439eb (diff) | |
| parent | 7e8fbed8df5e3f819e4775df791fc85f235854fb (diff) | |
Merge PR #9983: Hypothesis conversion allocates a single evar
Reviewed-by: gares
Ack-by: herbelin
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 3019fc0231..70854e6e3c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -515,6 +515,6 @@ let autounfold_one db cl = if did then match cl with | Some hyp -> change_in_hyp None (make_change_arg c') hyp - | None -> convert_concl_no_check c' DEFAULTcast + | None -> convert_concl ~check:false c' DEFAULTcast else Tacticals.New.tclFAIL 0 (str "Nothing to unfold") end |