diff options
| author | coqbot-app[bot] | 2020-11-05 15:32:31 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-05 15:32:31 +0000 |
| commit | afc828b3e207dd39c59d1501d570a88b2012fd2c (patch) | |
| tree | f9af32a8b25439a9eb6c8407f99ad94f78a64fda /vernac | |
| parent | b95c38d3d28a59da7ff7474ece0cb42623497b7d (diff) | |
| parent | e6f7517be65e9f5d2127a86e2213eb717d37e43f (diff) | |
Merge PR #12218: Numeral notations for non inductive types
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 123ea2c24e..efe4e17d0b 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -408,8 +408,8 @@ match e with | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists } | TTBigint -> begin match forpat with - | ForConstr -> push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v))) - | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v))) + | ForConstr -> push_constr subst (CAst.make @@ CPrim (Number (NumTok.Signed.of_int_string v))) + | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Number (NumTok.Signed.of_int_string v))) end | TTReference -> begin match forpat with |