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 /tactics | |
| parent | 2923b9262e3859f2ad0169778d63d79843d7ddf7 (diff) | |
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 6 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 2 |
2 files changed, 4 insertions, 4 deletions
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 |