diff options
| author | Pierre-Marie Pédrot | 2013-09-06 21:50:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-27 18:43:35 +0100 |
| commit | 144f2ac7c7394a701808daa503a0b6ded5663fcc (patch) | |
| tree | c193b3e8ba6d2650213e8c0cc4f0c52f14eedba3 /interp/constrextern.ml | |
| parent | 2923b9262e3859f2ad0169778d63d79843d7ddf7 (diff) | |
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 741ef9853a..ffb8a46ea1 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -597,13 +597,13 @@ let rec extern inctx scopes vars r = | GVar (loc,id) -> CRef (Ident (loc,id)) - | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None) + | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None) | GEvar (loc,n,l) -> extern_evar loc n (Option.map (List.map (extern false scopes vars)) l) | GPatVar (loc,n) -> - if !print_meta_as_hole then CHole (loc, None) else CPatVar (loc,n) + if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n) | GApp (loc,f,args) -> (match f with @@ -748,7 +748,7 @@ let rec extern inctx scopes vars r = | GSort (loc,s) -> CSort (loc,extern_glob_sort s) - | GHole (loc,e) -> CHole (loc, Some e) + | GHole (loc,e,_) -> CHole (loc, Some e, None) (** TODO: extern tactics. *) | GCast (loc,c, c') -> CCast (loc,sub_extern true scopes vars c, @@ -932,7 +932,7 @@ let extern_sort s = extern_glob_sort (detype_sort s) let any_any_branch = (* | _ => _ *) - (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole)) + (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,None)) let rec glob_of_pat env = function | PRef ref -> GRef (loc,ref) @@ -945,7 +945,7 @@ let rec glob_of_pat env = function anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar (loc,id) - | PMeta None -> GHole (loc,Evar_kinds.InternalHole) + | PMeta None -> GHole (loc,Evar_kinds.InternalHole, None) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args) |