Fixed a hole in glob_tactic that allowed some Ltac code to refer to

statically unbound variables (revealed by an assert failure in
Tacinterp.subst_rawconstr_and_expr). In particular, tauto's use of
name "id" was bypassing the globalization phase (apparently in an safe
way though).

Added a new kind of anomaly usable in case an anomaly results of an
unexpected exception.



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

5 files changed, 24 insertions, 6 deletions

diff --git a/lib/util.ml b/lib/util.ml
index ddf44eec37..2815af0145 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -20,6 +20,8 @@ exception UserError of string * std_ppcmds (* User errors *)
 let error string = raise (UserError(string, str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
+exception AnomalyOnError of string * exn
+
 let todo s = prerr_string ("TODO: "^s^"\n")
 
 exception Timeout
diff --git a/lib/util.mli b/lib/util.mli
index 4579982bcf..4e2bb6d339 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -26,6 +26,8 @@ exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
 
+exception AnomalyOnError of string * exn
+
 (* [todo] is for running of an incomplete code its implementation is
    "do nothing" (or print a message), but this function should not be
    used in a released code *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 427a6eaa67..ecf4ba9a53 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2899,7 +2899,8 @@ let add_tacdef isrec tacl =
 (***************************************************************************)
 (* Other entry points *)
 
-let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x
+let glob_tactic x =
+  Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
 
 let glob_tactic_env l env x =
   Flags.with_option strict_check
@@ -2916,7 +2917,10 @@ let interp_redexp env sigma r =
 (* Embed tactics in raw or glob tactic expr *)
 
 let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
-let tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist))
+let tacticIn t =
+  globTacticIn (fun ist ->
+    try glob_tactic (t ist)
+    with e -> raise (AnomalyOnError ("Incorrect tactic expression", e)))
 
 let tacticOut = function
   | TacArg (TacDynamic (_,d)) ->
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ebfb9446f3..6fea983772 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -20,6 +20,7 @@ open Tacticals
 open Tacinterp
 open Tactics
 open Util
+open Genarg
 
 let assoc_var s ist =
   match List.assoc (Names.id_of_string s) ist.lfun with
@@ -108,18 +109,21 @@ let is_conj ist =
 let flatten_contravariant_conj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then
 	let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in
+	let hyp = valueIn (VConstr hyp) in
 	let intros =
 	  iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
 	  <:tactic< idtac >> in
 	<:tactic<
           let newtyp := $newtyp in
-	  assert newtyp by ($intros; apply id; split; assumption);
-	  clear id
+          let hyp := $hyp in
+	  assert newtyp by ($intros; apply hyp; split; assumption);
+	  clear hyp
 	>>
       else
 	<:tactic<fail>>
@@ -140,16 +144,19 @@ let is_disj ist =
 let flatten_contravariant_disj ist =
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
+  let hyp = assoc_var "id" ist in
   match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with
   | Some (_,args) ->
       let i = List.length args in
       if not binary_mode || i = 2 then
+	let hyp = valueIn (VConstr hyp) in
 	iter_tac (list_map_i (fun i arg ->
 	  let typ = valueIn (VConstr (mkArrow arg c)) in
 	  <:tactic<
             let typ := $typ in
-	    assert typ by (intro; apply id; constructor $i; assumption)
-	  >>) 1 args) <:tactic< clear id >>
+            let hyp := $hyp in
+	    assert typ by (intro; apply hyp; constructor $i; assumption)
+	  >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >>
       else
 	<:tactic<fail>>
   | _ ->
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index dfedc178fb..08c0bac1c8 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -49,6 +49,9 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Timeout!")
   | Anomaly (s,pps) ->
       hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+  | AnomalyOnError (s,exc) ->
+      hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++ 
+	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Match_failure(filename,pos1,pos2) ->
       hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++
       if Sys.ocaml_version = "3.06" then