From 144f2ac7c7394a701808daa503a0b6ded5663fcc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 6 Sep 2013 21:50:35 +0200
Subject: Adding generic solvers to term holes. For now, no resolution
 mechanism nor parsing is plugged.

---
 interp/constrextern.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'interp/constrextern.ml')

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)
-- 
cgit v1.2.3