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.

---
 tactics/extratactics.ml4 | 6 +++---
 tactics/rewrite.ml       | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1c7b8d49f6..c81e7ce3f1 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -554,7 +554,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
 	      GHole (Loc.make_loc (!locref,0),
-		     Evar_kinds.QuestionMark(Evar_kinds.Define true))))
+		     Evar_kinds.QuestionMark(Evar_kinds.Define true), None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
   let t' = substrec t
@@ -565,13 +565,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true)) ->
+    | GHole (_,Evar_kinds.QuestionMark(Evar_kinds.Define true),s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
 	   GHole (Loc.make_loc (!locref,0),
-		  Evar_kinds.QuestionMark(Evar_kinds.Define true)))
+		  Evar_kinds.QuestionMark(Evar_kinds.Define true),s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 337ae52416..2e3b6e1af7 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1511,7 +1511,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CHole (Loc.ghost, None)
+let cHole = CHole (Loc.ghost, None, None)
 
 let proper_projection r ty =
   let ctx, inst = decompose_prod_assum ty in
-- 
cgit v1.2.3