diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-24 21:55:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-30 15:08:22 +0200 |
| commit | bbde815f8108f4641f5411d03f7a88096cc2221b (patch) | |
| tree | bc46ccddc767bb65bf836fd978b5779d4b2e3d78 /tactics/hipattern.ml | |
| parent | 5a86aabf4375b5f6f205dd328454748d2bc1217f (diff) | |
Support for using type information to infer more precise evar sources.
This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).
Incidentally updating output of Show output test (evar numbers shifted).
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index fd5eabe64..35fbec5a6 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -254,7 +254,7 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = CAst.make @@ GApp (f, args) let mkGHole = CAst.make @@ - GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None) + GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) let mkGProd id c1 c2 = CAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = CAst.make @@ |