Small fixes in "varify", a small tactic doing the first part of

reification: putting variables in a varmap.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11376 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 6 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 76d21b98ce..b50c591898 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1876,17 +1876,20 @@ let varify_constr_varmap ty def varh c =
   let vars = Idset.elements (freevars c) in
   let mkaccess i = 
     mkApp (Lazy.force coq_varmap_lookup,
-	  [| ty; def; mkidx i 1; varh |])
+	  [| ty; def; i; varh |])
   in
-  let rec vmap_aux l = 
+  let rec vmap_aux l cont = 
     match l with 
-    | [] -> mkApp (Lazy.force coq_varmap_empty, [| ty |])
+    | [] -> [], mkApp (Lazy.force coq_varmap_empty, [| ty |])
     | hd :: tl -> 
 	let left, right = split_interleaved [] [] tl in
-	  mkApp (Lazy.force coq_varmap_node, [| ty; hd; vmap_aux left ; vmap_aux right |])
+	let leftvars, leftmap = vmap_aux left (fun x -> cont (mkApp (Lazy.force coq_index_left, [| x |]))) in
+	let rightvars, rightmap = vmap_aux right (fun x -> cont (mkApp (Lazy.force coq_index_right, [| x |]))) in
+	  (hd, cont (Lazy.force coq_index_end)) :: leftvars @ rightvars, 
+	mkApp (Lazy.force coq_varmap_node, [| ty; hd; leftmap ; rightmap |])
   in
-  let vmap = vmap_aux (def :: List.map (fun x -> mkVar x) vars) in
-  let subst = list_map_i (fun i id -> (id, mkaccess i)) 0 vars in
+  let subst, vmap = vmap_aux (def :: List.map (fun x -> mkVar x) vars) (fun x -> x) in
+  let subst = List.map (fun (id, x) -> (destVar id, mkaccess x)) (List.tl subst) in
     vmap, replace_vars subst c