diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:01:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:21:25 +0100 |
| commit | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch) | |
| tree | 45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /interp | |
| parent | cca57bcd89770e76e1bcc21eb41756dca2c51425 (diff) | |
| parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) | |
Merge branch 'master'.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/topconstr.ml | 5 |
2 files changed, 6 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bac97aa3f..7eeb81050 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1739,7 +1739,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let k = match k with | None -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - Evar_kinds.QuestionMark st + (match naming with + | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id + | _ -> Evar_kinds.QuestionMark st) | Some k -> k in let solve = match solve with diff --git a/interp/topconstr.ml b/interp/topconstr.ml index b455381ea..407cec084 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -92,8 +92,9 @@ let rec fold_local_binders g f n acc b = function f n (fold_local_binders g f n' acc b l) t | LocalRawDef ((_,na),t)::l -> f n (fold_local_binders g f (name_fold g na n) acc b l) t - | LocalPattern _::l -> - assert false + | LocalPattern (_,pat,t)::l -> + let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in + Option.fold_left (f n) acc t | [] -> f n acc b |