Using the whole tactic environment while Pretyping.

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

5 files changed, 13 insertions, 31 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 87efaca199..ec8794e468 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -632,14 +632,11 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   else if Id.equal id ldots_var
   then
     if ntnvars != [] then GVar (loc,id), [], [], [] else error_ldots_var loc
+  else if Id.Map.mem id unbndltacvars then
+    (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
+    user_err_loc (loc,"intern_var",
+      str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
-  (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
-  try
-    match Id.Map.find id unbndltacvars with
-      | None -> user_err_loc (loc,"intern_var",
-	  str "variable " ++ pr_id id ++ str " should be bound to a term.")
-      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
-  with Not_found ->
     (* Is [id] a goal or section variable *)
     let _ = Context.lookup_named id namedctx in
       try
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4c51cffe1e..61f618c409 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -46,7 +46,7 @@ open Misctypes
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 type var_map = constr_under_binders Id.Map.t
-type unbound_ltac_var_map = Id.t option Id.Map.t
+type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
@@ -254,12 +254,10 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id =
 	  { uj_val  = mkVar id; uj_type = typ }
       with Not_found ->
 	(* [id] not found, build nice error message if [id] yet known from ltac *)
-	try
-	  match Id.Map.find id unbndltacvars with
-	  | None -> user_err_loc (loc,"",
-				  str "Variable " ++ pr_id id ++ str " should be bound to a term.")
-	  | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
-	with Not_found ->
+	if Id.Map.mem id unbndltacvars then
+	  user_err_loc (loc,"",
+            str "Variable " ++ pr_id id ++ str " should be bound to a term.")
+        else
 	  (* [id] not found, standard error message *)
 	  error_var_not_found_loc loc id
 
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 8a0b1f8862..98306e57f7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -29,7 +29,7 @@ val search_guard :
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
 type var_map = Pattern.constr_under_binders Id.Map.t
-type unbound_ltac_var_map = Id.t option Id.Map.t
+type unbound_ltac_var_map = Genarg.tlevel Genarg.generic_argument Id.Map.t
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b32e6731ee..7470de6c93 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -406,15 +406,7 @@ let extract_ltac_constr_values ist env =
       let c = coerce_to_constr env v in
       (Id.Map.add id c vars1, vars2)
     with CannotCoerceTo _ ->
-      let ido =
-        let v = Value.normalize v in
-        if has_type v (topwit wit_intro_pattern) then
-          match out_gen (topwit wit_intro_pattern) v with
-          | _, IntroIdentifier id0 -> Some id0
-          | _ -> None
-        else None
-      in
-      (vars1, Id.Map.add id ido vars2)
+      (vars1, Id.Map.add id v vars2)
   in
   Id.Map.fold fold ist.lfun (Id.Map.empty, Id.Map.empty)
 (** ppedrot: I have changed the semantics here. Before this patch, closure was
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 66eda3e80c..616dfb9417 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1076,18 +1076,13 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	   quote (Pptactic.pr_glob_tactic (Global.env())
 		    (Tacexpr.TacAtom (Loc.ghost,te)))
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
-          let fold id v accu = match v with
-          | None -> accu
-          | Some id' -> (id, ([], mkVar id')) :: accu
-          in
-          let unboundvars = Id.Map.fold fold unboundvars [] in
 	   quote (pr_glob_constr_env (Global.env()) c) ++
-	     (if not (List.is_empty unboundvars) || not (Id.Map.is_empty vars) then
+	     (if not (Id.Map.is_empty vars) then
 		strbrk " (with " ++
 		  prlist_with_sep pr_comma
 		  (fun (id,c) ->
 		     pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-		  (List.rev (Id.Map.bindings vars) @ unboundvars) ++ str ")"
+		  (List.rev (Id.Map.bindings vars)) ++ str ")"
 	      else mt())) ++
       (if Int.equal n 2 then str " (repeated twice)"
        else if n>2 then str " (repeated "++int n++str" times)"