- Fixing bug 1703 ("intros until n" falls back on the variable name when

  the latter is bound to a var which is not a quantified one - this led
  to remove a line marked "temporary compatibility" ... ; made a distinction
  between quantified hypothesis as for "intros until" and binding names as
  in "apply with"; in both cases, we now expect that a identifier not used 
  as a variable, as in "apply f_equal with f:=g" where "f" is a true binder
  name in f_equal, must not be used as a variable elsewhere [see
  corresponding change in Ints/Tactic.v])
- Fixing bug 1643 (bug in the algorithm used to possibly reuse a
  global name in the recursive calls of a coinductive term)
- Fixing bug 1699 (bug in contracting nested patterns at printing time
  when the return clause of the subpatterns is dependent)
- Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic)
- Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern)



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

1 files changed, 25 insertions, 10 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 77d9c265f4..884afebb9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -450,9 +450,16 @@ let rec intern_intro_pattern lf ist = function
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
 
-let intern_quantified_hypothesis ist x =
-  (* We use identifier both for variables and quantified hyps (no way to
-     statically check the existence of a quantified hyp); thus nothing to do *)
+let intern_quantified_hypothesis ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
+      NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
+      
+let intern_binding_name ist x =
+  (* We use identifier both for variables and binding names *)
+  (* Todo: consider the body of the lemma to which the binding refer 
+     and if a term w/o ltac vars, check the name is indeed quantified *)
   x
 
 let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
@@ -467,7 +474,7 @@ let intern_type = intern_constr_gen true
 
 (* Globalize bindings *)
 let intern_binding ist (loc,b,c) =
-  (loc,intern_quantified_hypothesis ist b,intern_constr ist c)
+  (loc,intern_binding_name ist b,intern_constr ist c)
 
 let intern_bindings ist = function
   | NoBindings -> NoBindings
@@ -1518,9 +1525,16 @@ let interp_quantified_hypothesis ist = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
-      with Not_found 
-      | Stdpp.Exc_located (_, UserError _) | UserError _ (*Compat provisoire*)
-   -> NamedHyp id
+      with Not_found -> NamedHyp id
+
+let interp_binding_name ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* If a name is bound, it has to be a quantified hypothesis *)
+      (* user has to use other names for variables if these ones clash with *)
+      (* a name intented to be used as a (non-variable) identifier *)
+      try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+      with Not_found -> NamedHyp id
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
@@ -1548,7 +1562,7 @@ let interp_induction_arg ist gl = function
 	(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
 
 let interp_binding ist gl (loc,b,c) =
-  (loc,interp_quantified_hypothesis ist b,pf_interp_open_constr false ist gl c)
+  (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c)
 
 let interp_bindings ist gl = function
 | NoBindings -> NoBindings
@@ -1803,7 +1817,7 @@ and interp_match_context ist g lz lr lmr =
 	    errorlabstrm "Tacinterp.apply_match_context"
               (v 0 (str "No matching clauses for match goal" ++
 		      (if ist.debug=DebugOff then
-			 fnl() ++ str "(use \"Debug On\" for more info)"
+			 fnl() ++ str "(use \"Set Ltac Debug\" for more info)"
 		       else mt())))
     end in
   let env = pf_env g in
@@ -2405,7 +2419,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l)
   | TacCut c -> TacCut (subst_rawconstr subst c)
-  | TacAssert (b,na,c) -> TacAssert (b,na,subst_rawconstr subst c)
+  | TacAssert (b,na,c) ->
+      TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c)
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)