Finish adding out-of-the-box support for camlp4

 If you want to try, it should be now as simple as:

 make clean && ./configure -local -usecamlp4 && make

 For the moment, the default stays camlp5, hence
 ./configure -usecamlp5 and ./configure are equivalent.

 Thanks to a suggestion by N. Pouillard, the remaining
 incompatibilities are now handled via some token filtering in
 camlp4. See compat5*.mlp. Morally, these files should be named .ml4,
 but I prefer having them not in $(...ML4) variables, it might confuse
 the Makefile... The empty compat5*.ml are used to build empty .cmo
 for making camlp5 happy. For camlp4,

 - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded
 - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with
    syntax such that VERNAC EXTEND, we only load it for a few files via
    camlp4deps

 TODO: check that my quick adaptation of camlp5-specific code in
 tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur
 is hiding information in the locations ?!

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

1 files changed, 5 insertions, 4 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0ddb4da75..e71e6366c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
 open Termops
 open Evd
 open Equality
+open Compat
 
 (**********************************************************************)
 (* replace, discriminate, injection, simplify_eq                      *)
@@ -543,7 +544,7 @@ let subst_var_with_hole occ tid t =
     | RVar (_,id) as x -> 
         if id = tid 
         then (decr occref; if !occref = 0 then x
-                           else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
+                           else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
         else x
     | c -> map_rawconstr_left_to_right substrec c in
   let t' = substrec t
@@ -556,7 +557,7 @@ let subst_hole_with_term occ tc t =
   let rec substrec = function
     | RHole (_,Evd.QuestionMark(Evd.Define true)) -> 
         decr occref; if !occref = 0 then tc
-                     else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
+                     else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
     | c -> map_rawconstr_left_to_right substrec c
   in
   substrec t
@@ -578,8 +579,8 @@ let hResolve id c occ t gl =
     try 
       Pretyping.Default.understand sigma env t_hole
     with 
-    | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> 
-        resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
+    | Loc.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
+        resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in