diff options
| author | ppedrot | 2013-06-24 12:56:39 +0000 |
|---|---|---|
| committer | ppedrot | 2013-06-24 12:56:39 +0000 |
| commit | 1c5f5f658c95def5cf19fdf5fdb2fe0a0aa1c740 (patch) | |
| tree | 432ad929d1ed065dff0b87c1325d9eaf09a82f01 /toplevel | |
| parent | 03ae5e5a2feccb80e5510f9b0cd02db06bef484f (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 9 |
1 files changed, 2 insertions, 7 deletions
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)" |