aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-07-27 16:05:34 +0200
committerPierre-Marie Pédrot2017-07-27 16:05:34 +0200
commit6b3fd33d7e3b775ce6afe38f7b16d4b11bdccdb3 (patch)
tree6f6d473e6852e61253e5e89ea6847ca7e9689076 /src
parentf204058d329fa78b506f4c3b3c4f97ecce504d4b (diff)
Fix expansion of toplevel let-rec after the constructor / constant split.
Diffstat (limited to 'src')
-rw-r--r--src/tac2entries.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index da0e213340..6fce739d30 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -269,8 +269,7 @@ let inline_rec_tactic tactics =
let map_body ((loc, id), _, e) = (loc, Name id), None, e in
let bnd = List.map map_body tactics in
let pat_of_id (loc, id) =
- let qid = (loc, qualid_of_ident id) in
- (CPatRef (Option.default dummy_loc loc, RelId qid, []), None)
+ (CPatVar (loc, Name id), None)
in
let var_of_id (loc, id) =
let qid = (loc, qualid_of_ident id) in