diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 18d6c1a5b7..715823e5d0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -552,7 +552,7 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = let is_var store pat = match DAst.get pat with - | PatVar na -> store na; true + | PatVar na -> ignore(store na); true | _ -> false let out_var pat = @@ -566,7 +566,7 @@ let term_of_name = function | Name id -> DAst.make (GVar id) | Anonymous -> let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None)) + DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None)) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous @@ -1370,7 +1370,8 @@ let sort_fields ~complete loc fields completer = (* the order does not matter as we sort them next, List.rev_* is just for efficiency *) let remaining_fields = - let complete_field (idx, _field_ref) = (idx, completer idx) in + let complete_field (idx, field_ref) = (idx, + completer idx field_ref record.Recordops.s_CONST) in List.rev_map complete_field remaining_projs in List.rev_append remaining_fields acc in @@ -1524,7 +1525,7 @@ let drop_notations_pattern looked_for genv = | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) | CPatRecord l -> let sorted_fields = - sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in + sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in begin match sorted_fields with | None -> DAst.make ?loc @@ RCPatAtom None | Some (n, head, pl) -> @@ -1890,9 +1891,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_applied_reference intern env (Environ.named_context globalenv) lvar us args ref in - (* Rem: GApp(_,f,[]) stands for @f *) - DAst.make ?loc @@ - GApp (f, intern_args env args_scopes (List.map fst args)) + (* Rem: GApp(_,f,[]) stands for @f *) + if args = [] then DAst.make ?loc @@ GApp (f,[]) else + smart_gapp f loc (intern_args env args_scopes (List.map fst args)) | CApp ((isproj,f), args) -> let f,args = match f.CAst.v with @@ -1918,8 +1919,16 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in let fields = sort_fields ~complete:true loc fs - (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)), - IntroAnonymous, None)) + (fun _idx fieldname constructorname -> + let open Evar_kinds in + let fieldinfo : Evar_kinds.record_field = + {fieldname=fieldname; recordname=inductive_of_constructor constructorname} + in + CAst.make ?loc @@ CHole (Some + (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with + Evar_kinds.qm_obligation=st; + Evar_kinds.qm_record_field=Some fieldinfo + }) , IntroAnonymous, None)) in begin match fields with @@ -2002,7 +2011,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in (match naming with | IntroIdentifier id -> Evar_kinds.NamedHole id - | _ -> Evar_kinds.QuestionMark (st,Anonymous)) + | _ -> Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st; }) | Some k -> k in let solve = match solve with @@ -2050,6 +2059,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CProj (pr, c) -> match intern_reference pr with | ConstRef p -> + let p = Option.get @@ Recordops.find_primitive_projection p in DAst.make ?loc @@ GProj (Projection.make p false, intern env c) | _ -> raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) |